doc-src/IsarRef/pure.tex
changeset 14934 bf9f525d4821
parent 14817 321ff6bf29d1
child 14955 08ee855c1d94
--- a/doc-src/IsarRef/pure.tex	Sun Jun 13 15:28:46 2004 +0200
+++ b/doc-src/IsarRef/pure.tex	Sun Jun 13 15:30:08 2004 +0200
@@ -1507,7 +1507,8 @@
 \subsection{System operations}
 
 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
-\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
+\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}\indexisarcmd{display-drafts}
+\indexisarcmd{print-drafts}
 \begin{matharray}{rcl}
   \isarcmd{cd}^* & : & \isarkeep{\cdot} \\
   \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\
@@ -1515,6 +1516,8 @@
   \isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\
   \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\
   \isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\
+  \isarcmd{display_drafts}^* & : & \isarkeep{\cdot} \\
+  \isarcmd{print_drafts}^* & : & \isarkeep{\cdot} \\
 \end{matharray}
 
 \begin{descr}
@@ -1528,6 +1531,10 @@
     implicit theory context to that of the theory loaded.}  (see also
   \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
   load new- and old-style theories alike.
+\item [$\isarkeyword{display_drafts} and \isarkeyword{print_drafts}$] perform
+  simple output of a given list of raw source files (specified as repeated
+  $name$ arguments).  Only those symbols that do not require additional LaTeX
+  packages are displayed properly, everything else is left verbatim.
 \end{descr}
 
 These system commands are scarcely used when working with the Proof~General