[Hol-checkins] [mn200/HOL] 695561: Document export_mono in the help system. Closes #...

[GitHub <no...@gi...>]

  Branch: refs/heads/master
  Home:   https://github.com/mn200/HOL
  Commit: 695561718a2afbc079507348a358ef29c2510d43
      https://github.com/mn200/HOL/commit/695561718a2afbc079507348a358ef29c2510d43
  Author: Michael Norrish <mic...@ni...>
  Date:   2012-07-25 (Wed, 25 Jul 2012)

  Changed paths:
    A help/Docfiles/IndDefLib.export_mono.doc

  Log Message:
  -----------
  Document export_mono in the help system.  Closes #66