updated generated file;
authorwenzelm
Mon Jun 02 23:38:28 2008 +0200 (2008-06-02)
changeset 270525c48cecb981b
parent 27051 a53dfe909674
child 27053 d58b0fd31b59
updated generated file;
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/IsarRef/Thy/document/Introduction.tex
doc-src/IsarRef/Thy/document/Misc.tex
doc-src/IsarRef/Thy/document/Outer_Syntax.tex
doc-src/IsarRef/Thy/document/Spec.tex
doc-src/IsarRef/Thy/document/pure.tex
     1.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Jun 02 23:38:27 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Jun 02 23:38:28 2008 +0200
     1.3 @@ -78,6 +78,7 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{matharray}{rcl}
     1.7 +    \indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isarkeep{toplevel} \\[0.5ex]
     1.8      \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isarkeep{local{\dsh}theory} \\
     1.9      \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isarkeep{local{\dsh}theory} \\
    1.10      \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
    1.11 @@ -99,12 +100,17 @@
    1.12    \begin{rail}
    1.13      ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
    1.14      ;
    1.15 -    ('text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
    1.16 +    ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
    1.17      ;
    1.18    \end{rail}
    1.19  
    1.20    \begin{descr}
    1.21  
    1.22 +  \item [\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
    1.23 +  markup just preceding the formal beginning of a theory.  In actual
    1.24 +  document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
    1.25 +  headings.  See also \secref{sec:markup} for further markup commands.
    1.26 +  
    1.27    \item [\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}, and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}] mark chapter and
    1.28    section headings.
    1.29  
     2.1 --- a/doc-src/IsarRef/Thy/document/Introduction.tex	Mon Jun 02 23:38:27 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Introduction.tex	Mon Jun 02 23:38:28 2008 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  \isatagtheory
     2.5  \isacommand{theory}\isamarkupfalse%
     2.6  \ Introduction\isanewline
     2.7 -\isakeyword{imports}\ Pure\isanewline
     2.8 +\isakeyword{imports}\ Main\isanewline
     2.9  \isakeyword{begin}%
    2.10  \endisatagtheory
    2.11  {\isafoldtheory}%
    2.12 @@ -92,7 +92,7 @@
    2.13  \end{isamarkuptext}%
    2.14  \isamarkuptrue%
    2.15  %
    2.16 -\isamarkupsection{Quick start%
    2.17 +\isamarkupsection{User interfaces%
    2.18  }
    2.19  \isamarkuptrue%
    2.20  %
    2.21 @@ -255,7 +255,7 @@
    2.22  \end{isamarkuptext}%
    2.23  \isamarkuptrue%
    2.24  %
    2.25 -\isamarkupsubsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
    2.26 +\isamarkupsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
    2.27  }
    2.28  \isamarkuptrue%
    2.29  %
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarRef/Thy/document/Misc.tex	Mon Jun 02 23:38:28 2008 +0200
     3.3 @@ -0,0 +1,287 @@
     3.4 +%
     3.5 +\begin{isabellebody}%
     3.6 +\def\isabellecontext{Misc}%
     3.7 +%
     3.8 +\isadelimtheory
     3.9 +\isanewline
    3.10 +\isanewline
    3.11 +%
    3.12 +\endisadelimtheory
    3.13 +%
    3.14 +\isatagtheory
    3.15 +\isacommand{theory}\isamarkupfalse%
    3.16 +\ Misc\isanewline
    3.17 +\isakeyword{imports}\ Main\isanewline
    3.18 +\isakeyword{begin}%
    3.19 +\endisatagtheory
    3.20 +{\isafoldtheory}%
    3.21 +%
    3.22 +\isadelimtheory
    3.23 +%
    3.24 +\endisadelimtheory
    3.25 +%
    3.26 +\isamarkupchapter{Other commands \label{ch:pure-syntax}%
    3.27 +}
    3.28 +\isamarkuptrue%
    3.29 +%
    3.30 +\isamarkupsection{Diagnostics%
    3.31 +}
    3.32 +\isamarkuptrue%
    3.33 +%
    3.34 +\begin{isamarkuptext}%
    3.35 +\begin{matharray}{rcl}
    3.36 +    \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
    3.37 +    \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    3.38 +    \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    3.39 +    \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    3.40 +    \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    3.41 +    \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    3.42 +    \indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    3.43 +  \end{matharray}
    3.44 +
    3.45 +  These diagnostic commands assist interactive development.  Note that
    3.46 +  \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} does not apply here, the theory or proof
    3.47 +  configuration is not changed.
    3.48 +
    3.49 +  \begin{rail}
    3.50 +    'pr' modes? nat? (',' nat)?
    3.51 +    ;
    3.52 +    'thm' modes? thmrefs
    3.53 +    ;
    3.54 +    'term' modes? term
    3.55 +    ;
    3.56 +    'prop' modes? prop
    3.57 +    ;
    3.58 +    'typ' modes? type
    3.59 +    ;
    3.60 +    'prf' modes? thmrefs?
    3.61 +    ;
    3.62 +    'full\_prf' modes? thmrefs?
    3.63 +    ;
    3.64 +
    3.65 +    modes: '(' (name + ) ')'
    3.66 +    ;
    3.67 +  \end{rail}
    3.68 +
    3.69 +  \begin{descr}
    3.70 +
    3.71 +  \item [\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}}] prints the current
    3.72 +  proof state (if present), including the proof context, current facts
    3.73 +  and goals.  The optional limit arguments affect the number of goals
    3.74 +  and premises to be displayed, which is initially 10 for both.
    3.75 +  Omitting limit values leaves the current setting unchanged.
    3.76 +
    3.77 +  \item [\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] retrieves
    3.78 +  theorems from the current theory or proof context.  Note that any
    3.79 +  attributes included in the theorem specifications are applied to a
    3.80 +  temporary context derived from the current theory or proof; the
    3.81 +  result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect.
    3.82 +
    3.83 +  \item [\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}}]
    3.84 +  read, type-check and print terms or propositions according to the
    3.85 +  current theory or proof context; the inferred type of \isa{t} is
    3.86 +  output as well.  Note that these commands are also useful in
    3.87 +  inspecting the current environment of term abbreviations.
    3.88 +
    3.89 +  \item [\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}}] reads and prints types of the
    3.90 +  meta-logic according to the current theory or proof context.
    3.91 +
    3.92 +  \item [\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}] displays the (compact) proof term of the
    3.93 +  current proof state (if present), or of the given theorems. Note
    3.94 +  that this requires proof terms to be switched on for the current
    3.95 +  object logic (see the ``Proof terms'' section of the Isabelle
    3.96 +  reference manual for information on how to do this).
    3.97 +
    3.98 +  \item [\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
    3.99 +  the full proof term, i.e.\ also displays information omitted in the
   3.100 +  compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
   3.101 +  there.
   3.102 +
   3.103 +  \end{descr}
   3.104 +
   3.105 +  All of the diagnostic commands above admit a list of \isa{modes}
   3.106 +  to be specified, which is appended to the current print mode (see
   3.107 +  also \cite{isabelle-ref}).  Thus the output behavior may be modified
   3.108 +  according particular print mode features.  For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}{\isachardoublequote}} would print the current
   3.109 +  proof state with mathematical symbols and special characters
   3.110 +  represented in {\LaTeX} source, according to the Isabelle style
   3.111 +  \cite{isabelle-sys}.
   3.112 +
   3.113 +  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
   3.114 +  systematic way to include formal items into the printed text
   3.115 +  document.%
   3.116 +\end{isamarkuptext}%
   3.117 +\isamarkuptrue%
   3.118 +%
   3.119 +\isamarkupsection{Inspecting the context%
   3.120 +}
   3.121 +\isamarkuptrue%
   3.122 +%
   3.123 +\begin{isamarkuptext}%
   3.124 +\begin{matharray}{rcl}
   3.125 +    \indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   3.126 +    \indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   3.127 +    \indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   3.128 +    \indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   3.129 +    \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   3.130 +    \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   3.131 +    \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   3.132 +    \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   3.133 +    \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
   3.134 +    \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
   3.135 +  \end{matharray}
   3.136 +
   3.137 +  \begin{rail}
   3.138 +    'print\_theory' ( '!'?)
   3.139 +    ;
   3.140 +
   3.141 +    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
   3.142 +    ;
   3.143 +    criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
   3.144 +      'simp' ':' term | term)
   3.145 +    ;
   3.146 +    'thm\_deps' thmrefs
   3.147 +    ;
   3.148 +  \end{rail}
   3.149 +
   3.150 +  These commands print certain parts of the theory and proof context.
   3.151 +  Note that there are some further ones available, such as for the set
   3.152 +  of rules declared for simplifications.
   3.153 +
   3.154 +  \begin{descr}
   3.155 +  
   3.156 +  \item [\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory
   3.157 +  syntax, including keywords and command.
   3.158 +  
   3.159 +  \item [\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of
   3.160 +  the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra
   3.161 +  verbosity.
   3.162 +
   3.163 +  \item [\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types
   3.164 +  and terms, depending on the current context.  The output can be very
   3.165 +  verbose, including grammar tables and syntax translation rules.  See
   3.166 +  \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
   3.167 +  inner syntax.
   3.168 +  
   3.169 +  \item [\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods
   3.170 +  available in the current theory context.
   3.171 +  
   3.172 +  \item [\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes
   3.173 +  available in the current theory context.
   3.174 +  
   3.175 +  \item [\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from
   3.176 +  the last command.
   3.177 +  
   3.178 +  \item [\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts
   3.179 +  from the theory or proof context matching all of given search
   3.180 +  criteria.  The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems
   3.181 +  whose fully qualified name matches pattern \isa{p}, which may
   3.182 +  contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards.  The criteria \isa{intro},
   3.183 +  \isa{elim}, and \isa{dest} select theorems that match the
   3.184 +  current goal as introduction, elimination or destruction rules,
   3.185 +  respectively.  The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite
   3.186 +  rules whose left-hand side matches the given term.  The criterion
   3.187 +  term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
   3.188 +  ``\isa{{\isacharunderscore}}'', schematic variables, and type constraints.
   3.189 +  
   3.190 +  Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that
   3.191 +  do \emph{not} match. Note that giving the empty list of criteria
   3.192 +  yields \emph{all} currently known facts.  An optional limit for the
   3.193 +  number of printed facts may be given; the default is 40.  By
   3.194 +  default, duplicates are removed from the search result. Use
   3.195 +  \isa{with{\isacharunderscore}dups} to display duplicates.
   3.196 +  
   3.197 +  \item [\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
   3.198 +  visualizes dependencies of facts, using Isabelle's graph browser
   3.199 +  tool (see also \cite{isabelle-sys}).
   3.200 +  
   3.201 +  \item [\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the
   3.202 +  current context, both named and unnamed ones.
   3.203 +  
   3.204 +  \item [\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations
   3.205 +  present in the context.
   3.206 +
   3.207 +  \end{descr}%
   3.208 +\end{isamarkuptext}%
   3.209 +\isamarkuptrue%
   3.210 +%
   3.211 +\isamarkupsection{History commands \label{sec:history}%
   3.212 +}
   3.213 +\isamarkuptrue%
   3.214 +%
   3.215 +\begin{isamarkuptext}%
   3.216 +\begin{matharray}{rcl}
   3.217 +    \indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
   3.218 +    \indexdef{}{command}{redo}\hypertarget{command.redo}{\hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
   3.219 +    \indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
   3.220 +  \end{matharray}
   3.221 +
   3.222 +  The Isabelle/Isar top-level maintains a two-stage history, for
   3.223 +  theory and proof state transformation.  Basically, any command can
   3.224 +  be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic
   3.225 +  elements.  Its effect may be revoked via \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, unless
   3.226 +  the corresponding \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} step has crossed the beginning
   3.227 +  of a proof or theory.  The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts the
   3.228 +  current history node altogether, discontinuing a proof or even the
   3.229 +  whole theory.  This operation is \emph{not} undo-able.
   3.230 +
   3.231 +  \begin{warn}
   3.232 +    History commands should never be used with user interfaces such as
   3.233 +    Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
   3.234 +    care of stepping forth and back itself.  Interfering by manual
   3.235 +    \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}
   3.236 +    commands would quickly result in utter confusion.
   3.237 +  \end{warn}%
   3.238 +\end{isamarkuptext}%
   3.239 +\isamarkuptrue%
   3.240 +%
   3.241 +\isamarkupsection{System operations%
   3.242 +}
   3.243 +\isamarkuptrue%
   3.244 +%
   3.245 +\begin{isamarkuptext}%
   3.246 +\begin{matharray}{rcl}
   3.247 +    \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   3.248 +    \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   3.249 +    \indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   3.250 +  \end{matharray}
   3.251 +
   3.252 +  \begin{rail}
   3.253 +    ('cd' | 'use\_thy' | 'update\_thy') name
   3.254 +    ;
   3.255 +  \end{rail}
   3.256 +
   3.257 +  \begin{descr}
   3.258 +
   3.259 +  \item [\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path}] changes the current directory
   3.260 +  of the Isabelle process.
   3.261 +
   3.262 +  \item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory.
   3.263 +
   3.264 +  \item [\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}.
   3.265 +  These system commands are scarcely used when working interactively,
   3.266 +  since loading of theories is done automatically as required.
   3.267 +
   3.268 +  \end{descr}%
   3.269 +\end{isamarkuptext}%
   3.270 +\isamarkuptrue%
   3.271 +%
   3.272 +\isadelimtheory
   3.273 +%
   3.274 +\endisadelimtheory
   3.275 +%
   3.276 +\isatagtheory
   3.277 +\isacommand{end}\isamarkupfalse%
   3.278 +%
   3.279 +\endisatagtheory
   3.280 +{\isafoldtheory}%
   3.281 +%
   3.282 +\isadelimtheory
   3.283 +%
   3.284 +\endisadelimtheory
   3.285 +\isanewline
   3.286 +\end{isabellebody}%
   3.287 +%%% Local Variables:
   3.288 +%%% mode: latex
   3.289 +%%% TeX-master: "root"
   3.290 +%%% End:
     4.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Mon Jun 02 23:38:27 2008 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Mon Jun 02 23:38:28 2008 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  \isatagtheory
     4.5  \isacommand{theory}\isamarkupfalse%
     4.6  \ Outer{\isacharunderscore}Syntax\isanewline
     4.7 -\isakeyword{imports}\ Pure\isanewline
     4.8 +\isakeyword{imports}\ Main\isanewline
     4.9  \isakeyword{begin}%
    4.10  \endisatagtheory
    4.11  {\isafoldtheory}%
     5.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Jun 02 23:38:27 2008 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Jun 02 23:38:28 2008 +0200
     5.3 @@ -30,7 +30,6 @@
     5.4  %
     5.5  \begin{isamarkuptext}%
     5.6  \begin{matharray}{rcl}
     5.7 -    \indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isarkeep{toplevel} \\
     5.8      \indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isartrans{toplevel}{theory} \\
     5.9      \indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\
    5.10    \end{matharray}
    5.11 @@ -45,14 +44,10 @@
    5.12    ones.  Just preceding the \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} keyword, there may be
    5.13    an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is relevant to
    5.14    document preparation only; it acts very much like a special
    5.15 -  pre-theory markup command (cf.\ \secref{sec:markup} and).  The
    5.16 -  \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command
    5.17 -  concludes a theory development; it has to be the very last command
    5.18 -  of any theory file loaded in batch-mode.
    5.19 +  pre-theory markup command (cf.\ \secref{sec:markup}).  The \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command concludes a theory development; it has to be
    5.20 +  the very last command of any theory file loaded in batch-mode.
    5.21  
    5.22    \begin{rail}
    5.23 -    'header' text
    5.24 -    ;
    5.25      'theory' name 'imports' (name +) uses? 'begin'
    5.26      ;
    5.27  
    5.28 @@ -61,11 +56,6 @@
    5.29  
    5.30    \begin{descr}
    5.31  
    5.32 -  \item [\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
    5.33 -  markup just preceding the formal beginning of a theory.  In actual
    5.34 -  document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
    5.35 -  headings.  See also \secref{sec:markup} for further markup commands.
    5.36 -  
    5.37    \item [\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] starts a new theory \isa{A} based on the
    5.38    merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.
    5.39    
    5.40 @@ -121,9 +111,9 @@
    5.41    
    5.42    \item [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an
    5.43    existing locale or class context \isa{c}.  Note that locale and
    5.44 -  class definitions allow to include the \indexref{}{keyword}{begin}\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}
    5.45 -  keyword as well, in order to continue the local theory immediately
    5.46 -  after the initial specification.
    5.47 +  class definitions allow to include the \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as
    5.48 +  well, in order to continue the local theory immediately after the
    5.49 +  initial specification.
    5.50    
    5.51    \item [\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current local theory
    5.52    and continues the enclosing global theory.  Note that a global
     6.1 --- a/doc-src/IsarRef/Thy/document/pure.tex	Mon Jun 02 23:38:27 2008 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,291 +0,0 @@
     6.4 -%
     6.5 -\begin{isabellebody}%
     6.6 -\def\isabellecontext{pure}%
     6.7 -%
     6.8 -\isadelimtheory
     6.9 -\isanewline
    6.10 -\isanewline
    6.11 -%
    6.12 -\endisadelimtheory
    6.13 -%
    6.14 -\isatagtheory
    6.15 -\isacommand{theory}\isamarkupfalse%
    6.16 -\ pure\isanewline
    6.17 -\isakeyword{imports}\ Pure\isanewline
    6.18 -\isakeyword{begin}%
    6.19 -\endisatagtheory
    6.20 -{\isafoldtheory}%
    6.21 -%
    6.22 -\isadelimtheory
    6.23 -%
    6.24 -\endisadelimtheory
    6.25 -%
    6.26 -\isamarkupchapter{Basic language elements \label{ch:pure-syntax}%
    6.27 -}
    6.28 -\isamarkuptrue%
    6.29 -%
    6.30 -\isamarkupsection{Other commands%
    6.31 -}
    6.32 -\isamarkuptrue%
    6.33 -%
    6.34 -\isamarkupsubsection{Diagnostics%
    6.35 -}
    6.36 -\isamarkuptrue%
    6.37 -%
    6.38 -\begin{isamarkuptext}%
    6.39 -\begin{matharray}{rcl}
    6.40 -    \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
    6.41 -    \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    6.42 -    \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    6.43 -    \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    6.44 -    \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    6.45 -    \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    6.46 -    \indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    6.47 -  \end{matharray}
    6.48 -
    6.49 -  These diagnostic commands assist interactive development.  Note that
    6.50 -  \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} does not apply here, the theory or proof
    6.51 -  configuration is not changed.
    6.52 -
    6.53 -  \begin{rail}
    6.54 -    'pr' modes? nat? (',' nat)?
    6.55 -    ;
    6.56 -    'thm' modes? thmrefs
    6.57 -    ;
    6.58 -    'term' modes? term
    6.59 -    ;
    6.60 -    'prop' modes? prop
    6.61 -    ;
    6.62 -    'typ' modes? type
    6.63 -    ;
    6.64 -    'prf' modes? thmrefs?
    6.65 -    ;
    6.66 -    'full\_prf' modes? thmrefs?
    6.67 -    ;
    6.68 -
    6.69 -    modes: '(' (name + ) ')'
    6.70 -    ;
    6.71 -  \end{rail}
    6.72 -
    6.73 -  \begin{descr}
    6.74 -
    6.75 -  \item [\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}}] prints the current
    6.76 -  proof state (if present), including the proof context, current facts
    6.77 -  and goals.  The optional limit arguments affect the number of goals
    6.78 -  and premises to be displayed, which is initially 10 for both.
    6.79 -  Omitting limit values leaves the current setting unchanged.
    6.80 -
    6.81 -  \item [\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] retrieves
    6.82 -  theorems from the current theory or proof context.  Note that any
    6.83 -  attributes included in the theorem specifications are applied to a
    6.84 -  temporary context derived from the current theory or proof; the
    6.85 -  result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect.
    6.86 -
    6.87 -  \item [\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}}]
    6.88 -  read, type-check and print terms or propositions according to the
    6.89 -  current theory or proof context; the inferred type of \isa{t} is
    6.90 -  output as well.  Note that these commands are also useful in
    6.91 -  inspecting the current environment of term abbreviations.
    6.92 -
    6.93 -  \item [\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}}] reads and prints types of the
    6.94 -  meta-logic according to the current theory or proof context.
    6.95 -
    6.96 -  \item [\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}] displays the (compact) proof term of the
    6.97 -  current proof state (if present), or of the given theorems. Note
    6.98 -  that this requires proof terms to be switched on for the current
    6.99 -  object logic (see the ``Proof terms'' section of the Isabelle
   6.100 -  reference manual for information on how to do this).
   6.101 -
   6.102 -  \item [\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
   6.103 -  the full proof term, i.e.\ also displays information omitted in the
   6.104 -  compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
   6.105 -  there.
   6.106 -
   6.107 -  \end{descr}
   6.108 -
   6.109 -  All of the diagnostic commands above admit a list of \isa{modes}
   6.110 -  to be specified, which is appended to the current print mode (see
   6.111 -  also \cite{isabelle-ref}).  Thus the output behavior may be modified
   6.112 -  according particular print mode features.  For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}{\isachardoublequote}} would print the current
   6.113 -  proof state with mathematical symbols and special characters
   6.114 -  represented in {\LaTeX} source, according to the Isabelle style
   6.115 -  \cite{isabelle-sys}.
   6.116 -
   6.117 -  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
   6.118 -  systematic way to include formal items into the printed text
   6.119 -  document.%
   6.120 -\end{isamarkuptext}%
   6.121 -\isamarkuptrue%
   6.122 -%
   6.123 -\isamarkupsubsection{Inspecting the context%
   6.124 -}
   6.125 -\isamarkuptrue%
   6.126 -%
   6.127 -\begin{isamarkuptext}%
   6.128 -\begin{matharray}{rcl}
   6.129 -    \indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   6.130 -    \indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   6.131 -    \indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   6.132 -    \indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   6.133 -    \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   6.134 -    \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   6.135 -    \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   6.136 -    \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   6.137 -    \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
   6.138 -    \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
   6.139 -  \end{matharray}
   6.140 -
   6.141 -  \begin{rail}
   6.142 -    'print\_theory' ( '!'?)
   6.143 -    ;
   6.144 -
   6.145 -    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
   6.146 -    ;
   6.147 -    criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
   6.148 -      'simp' ':' term | term)
   6.149 -    ;
   6.150 -    'thm\_deps' thmrefs
   6.151 -    ;
   6.152 -  \end{rail}
   6.153 -
   6.154 -  These commands print certain parts of the theory and proof context.
   6.155 -  Note that there are some further ones available, such as for the set
   6.156 -  of rules declared for simplifications.
   6.157 -
   6.158 -  \begin{descr}
   6.159 -  
   6.160 -  \item [\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory
   6.161 -  syntax, including keywords and command.
   6.162 -  
   6.163 -  \item [\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of
   6.164 -  the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra
   6.165 -  verbosity.
   6.166 -
   6.167 -  \item [\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types
   6.168 -  and terms, depending on the current context.  The output can be very
   6.169 -  verbose, including grammar tables and syntax translation rules.  See
   6.170 -  \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
   6.171 -  inner syntax.
   6.172 -  
   6.173 -  \item [\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods
   6.174 -  available in the current theory context.
   6.175 -  
   6.176 -  \item [\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes
   6.177 -  available in the current theory context.
   6.178 -  
   6.179 -  \item [\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from
   6.180 -  the last command.
   6.181 -  
   6.182 -  \item [\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts
   6.183 -  from the theory or proof context matching all of given search
   6.184 -  criteria.  The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems
   6.185 -  whose fully qualified name matches pattern \isa{p}, which may
   6.186 -  contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards.  The criteria \isa{intro},
   6.187 -  \isa{elim}, and \isa{dest} select theorems that match the
   6.188 -  current goal as introduction, elimination or destruction rules,
   6.189 -  respectively.  The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite
   6.190 -  rules whose left-hand side matches the given term.  The criterion
   6.191 -  term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
   6.192 -  ``\isa{{\isacharunderscore}}'', schematic variables, and type constraints.
   6.193 -  
   6.194 -  Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that
   6.195 -  do \emph{not} match. Note that giving the empty list of criteria
   6.196 -  yields \emph{all} currently known facts.  An optional limit for the
   6.197 -  number of printed facts may be given; the default is 40.  By
   6.198 -  default, duplicates are removed from the search result. Use
   6.199 -  \isa{with{\isacharunderscore}dups} to display duplicates.
   6.200 -  
   6.201 -  \item [\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
   6.202 -  visualizes dependencies of facts, using Isabelle's graph browser
   6.203 -  tool (see also \cite{isabelle-sys}).
   6.204 -  
   6.205 -  \item [\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the
   6.206 -  current context, both named and unnamed ones.
   6.207 -  
   6.208 -  \item [\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations
   6.209 -  present in the context.
   6.210 -
   6.211 -  \end{descr}%
   6.212 -\end{isamarkuptext}%
   6.213 -\isamarkuptrue%
   6.214 -%
   6.215 -\isamarkupsubsection{History commands \label{sec:history}%
   6.216 -}
   6.217 -\isamarkuptrue%
   6.218 -%
   6.219 -\begin{isamarkuptext}%
   6.220 -\begin{matharray}{rcl}
   6.221 -    \indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
   6.222 -    \indexdef{}{command}{redo}\hypertarget{command.redo}{\hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
   6.223 -    \indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
   6.224 -  \end{matharray}
   6.225 -
   6.226 -  The Isabelle/Isar top-level maintains a two-stage history, for
   6.227 -  theory and proof state transformation.  Basically, any command can
   6.228 -  be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic
   6.229 -  elements.  Its effect may be revoked via \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, unless
   6.230 -  the corresponding \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} step has crossed the beginning
   6.231 -  of a proof or theory.  The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts the
   6.232 -  current history node altogether, discontinuing a proof or even the
   6.233 -  whole theory.  This operation is \emph{not} undo-able.
   6.234 -
   6.235 -  \begin{warn}
   6.236 -    History commands should never be used with user interfaces such as
   6.237 -    Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
   6.238 -    care of stepping forth and back itself.  Interfering by manual
   6.239 -    \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}
   6.240 -    commands would quickly result in utter confusion.
   6.241 -  \end{warn}%
   6.242 -\end{isamarkuptext}%
   6.243 -\isamarkuptrue%
   6.244 -%
   6.245 -\isamarkupsubsection{System operations%
   6.246 -}
   6.247 -\isamarkuptrue%
   6.248 -%
   6.249 -\begin{isamarkuptext}%
   6.250 -\begin{matharray}{rcl}
   6.251 -    \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   6.252 -    \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   6.253 -    \indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   6.254 -  \end{matharray}
   6.255 -
   6.256 -  \begin{rail}
   6.257 -    ('cd' | 'use\_thy' | 'update\_thy') name
   6.258 -    ;
   6.259 -  \end{rail}
   6.260 -
   6.261 -  \begin{descr}
   6.262 -
   6.263 -  \item [\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path}] changes the current directory
   6.264 -  of the Isabelle process.
   6.265 -
   6.266 -  \item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory.
   6.267 -
   6.268 -  \item [\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}.
   6.269 -  These system commands are scarcely used when working interactively,
   6.270 -  since loading of theories is done automatically as required.
   6.271 -
   6.272 -  \end{descr}%
   6.273 -\end{isamarkuptext}%
   6.274 -\isamarkuptrue%
   6.275 -%
   6.276 -\isadelimtheory
   6.277 -%
   6.278 -\endisadelimtheory
   6.279 -%
   6.280 -\isatagtheory
   6.281 -\isacommand{end}\isamarkupfalse%
   6.282 -%
   6.283 -\endisatagtheory
   6.284 -{\isafoldtheory}%
   6.285 -%
   6.286 -\isadelimtheory
   6.287 -%
   6.288 -\endisadelimtheory
   6.289 -\isanewline
   6.290 -\end{isabellebody}%
   6.291 -%%% Local Variables:
   6.292 -%%% mode: latex
   6.293 -%%% TeX-master: "root"
   6.294 -%%% End: