doc-src/IsarRef/pure.tex
changeset 14934 bf9f525d4821
parent 14817 321ff6bf29d1
child 14955 08ee855c1d94
equal deleted inserted replaced
14933:3fd8c03e3ee6 14934:bf9f525d4821
  1505 
  1505 
  1506 
  1506 
  1507 \subsection{System operations}
  1507 \subsection{System operations}
  1508 
  1508 
  1509 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
  1509 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
  1510 \indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
  1510 \indexisarcmd{update-thy}\indexisarcmd{update-thy-only}\indexisarcmd{display-drafts}
       
  1511 \indexisarcmd{print-drafts}
  1511 \begin{matharray}{rcl}
  1512 \begin{matharray}{rcl}
  1512   \isarcmd{cd}^* & : & \isarkeep{\cdot} \\
  1513   \isarcmd{cd}^* & : & \isarkeep{\cdot} \\
  1513   \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\
  1514   \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\
  1514   \isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\
  1515   \isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\
  1515   \isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\
  1516   \isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\
  1516   \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\
  1517   \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\
  1517   \isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\
  1518   \isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\
       
  1519   \isarcmd{display_drafts}^* & : & \isarkeep{\cdot} \\
       
  1520   \isarcmd{print_drafts}^* & : & \isarkeep{\cdot} \\
  1518 \end{matharray}
  1521 \end{matharray}
  1519 
  1522 
  1520 \begin{descr}
  1523 \begin{descr}
  1521 \item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
  1524 \item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
  1522   process.
  1525   process.
  1526   theory given as $name$ argument.  These commands are basically the same as
  1529   theory given as $name$ argument.  These commands are basically the same as
  1527   the corresponding ML functions\footnote{The ML versions also change the
  1530   the corresponding ML functions\footnote{The ML versions also change the
  1528     implicit theory context to that of the theory loaded.}  (see also
  1531     implicit theory context to that of the theory loaded.}  (see also
  1529   \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
  1532   \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
  1530   load new- and old-style theories alike.
  1533   load new- and old-style theories alike.
       
  1534 \item [$\isarkeyword{display_drafts} and \isarkeyword{print_drafts}$] perform
       
  1535   simple output of a given list of raw source files (specified as repeated
       
  1536   $name$ arguments).  Only those symbols that do not require additional LaTeX
       
  1537   packages are displayed properly, everything else is left verbatim.
  1531 \end{descr}
  1538 \end{descr}
  1532 
  1539 
  1533 These system commands are scarcely used when working with the Proof~General
  1540 These system commands are scarcely used when working with the Proof~General
  1534 interface, since loading of theories is done transparently.
  1541 interface, since loading of theories is done transparently.
  1535 
  1542