doc-src/IsarRef/Thy/document/Misc.tex
author wenzelm
Tue Jun 03 00:03:54 2008 +0200 (2008-06-03)
changeset 27054 f1ef0973d0a8
parent 27052 5c48cecb981b
child 27598 b66e257b75f5
permissions -rw-r--r--
updated generated file;
wenzelm@27052
     1
%
wenzelm@27052
     2
\begin{isabellebody}%
wenzelm@27052
     3
\def\isabellecontext{Misc}%
wenzelm@27052
     4
%
wenzelm@27052
     5
\isadelimtheory
wenzelm@27052
     6
\isanewline
wenzelm@27052
     7
\isanewline
wenzelm@27052
     8
%
wenzelm@27052
     9
\endisadelimtheory
wenzelm@27052
    10
%
wenzelm@27052
    11
\isatagtheory
wenzelm@27052
    12
\isacommand{theory}\isamarkupfalse%
wenzelm@27052
    13
\ Misc\isanewline
wenzelm@27052
    14
\isakeyword{imports}\ Main\isanewline
wenzelm@27052
    15
\isakeyword{begin}%
wenzelm@27052
    16
\endisatagtheory
wenzelm@27052
    17
{\isafoldtheory}%
wenzelm@27052
    18
%
wenzelm@27052
    19
\isadelimtheory
wenzelm@27052
    20
%
wenzelm@27052
    21
\endisadelimtheory
wenzelm@27052
    22
%
wenzelm@27052
    23
\isamarkupchapter{Other commands \label{ch:pure-syntax}%
wenzelm@27052
    24
}
wenzelm@27052
    25
\isamarkuptrue%
wenzelm@27052
    26
%
wenzelm@27052
    27
\isamarkupsection{Diagnostics%
wenzelm@27052
    28
}
wenzelm@27052
    29
\isamarkuptrue%
wenzelm@27052
    30
%
wenzelm@27052
    31
\begin{isamarkuptext}%
wenzelm@27052
    32
\begin{matharray}{rcl}
wenzelm@27052
    33
    \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
wenzelm@27052
    34
    \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
wenzelm@27052
    35
    \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
wenzelm@27052
    36
    \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
wenzelm@27052
    37
    \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
wenzelm@27052
    38
    \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
wenzelm@27052
    39
    \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} \\
wenzelm@27052
    40
  \end{matharray}
wenzelm@27052
    41
wenzelm@27052
    42
  These diagnostic commands assist interactive development.  Note that
wenzelm@27052
    43
  \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} does not apply here, the theory or proof
wenzelm@27052
    44
  configuration is not changed.
wenzelm@27052
    45
wenzelm@27052
    46
  \begin{rail}
wenzelm@27052
    47
    'pr' modes? nat? (',' nat)?
wenzelm@27052
    48
    ;
wenzelm@27052
    49
    'thm' modes? thmrefs
wenzelm@27052
    50
    ;
wenzelm@27052
    51
    'term' modes? term
wenzelm@27052
    52
    ;
wenzelm@27052
    53
    'prop' modes? prop
wenzelm@27052
    54
    ;
wenzelm@27052
    55
    'typ' modes? type
wenzelm@27052
    56
    ;
wenzelm@27052
    57
    'prf' modes? thmrefs?
wenzelm@27052
    58
    ;
wenzelm@27052
    59
    'full\_prf' modes? thmrefs?
wenzelm@27052
    60
    ;
wenzelm@27052
    61
wenzelm@27052
    62
    modes: '(' (name + ) ')'
wenzelm@27052
    63
    ;
wenzelm@27052
    64
  \end{rail}
wenzelm@27052
    65
wenzelm@27052
    66
  \begin{descr}
wenzelm@27052
    67
wenzelm@27052
    68
  \item [\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}}] prints the current
wenzelm@27052
    69
  proof state (if present), including the proof context, current facts
wenzelm@27052
    70
  and goals.  The optional limit arguments affect the number of goals
wenzelm@27052
    71
  and premises to be displayed, which is initially 10 for both.
wenzelm@27052
    72
  Omitting limit values leaves the current setting unchanged.
wenzelm@27052
    73
wenzelm@27052
    74
  \item [\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] retrieves
wenzelm@27052
    75
  theorems from the current theory or proof context.  Note that any
wenzelm@27052
    76
  attributes included in the theorem specifications are applied to a
wenzelm@27052
    77
  temporary context derived from the current theory or proof; the
wenzelm@27052
    78
  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.
wenzelm@27052
    79
wenzelm@27052
    80
  \item [\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}}]
wenzelm@27052
    81
  read, type-check and print terms or propositions according to the
wenzelm@27052
    82
  current theory or proof context; the inferred type of \isa{t} is
wenzelm@27052
    83
  output as well.  Note that these commands are also useful in
wenzelm@27052
    84
  inspecting the current environment of term abbreviations.
wenzelm@27052
    85
wenzelm@27052
    86
  \item [\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}}] reads and prints types of the
wenzelm@27052
    87
  meta-logic according to the current theory or proof context.
wenzelm@27052
    88
wenzelm@27052
    89
  \item [\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}] displays the (compact) proof term of the
wenzelm@27052
    90
  current proof state (if present), or of the given theorems. Note
wenzelm@27052
    91
  that this requires proof terms to be switched on for the current
wenzelm@27052
    92
  object logic (see the ``Proof terms'' section of the Isabelle
wenzelm@27052
    93
  reference manual for information on how to do this).
wenzelm@27052
    94
wenzelm@27052
    95
  \item [\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
wenzelm@27052
    96
  the full proof term, i.e.\ also displays information omitted in the
wenzelm@27052
    97
  compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
wenzelm@27052
    98
  there.
wenzelm@27052
    99
wenzelm@27052
   100
  \end{descr}
wenzelm@27052
   101
wenzelm@27052
   102
  All of the diagnostic commands above admit a list of \isa{modes}
wenzelm@27052
   103
  to be specified, which is appended to the current print mode (see
wenzelm@27052
   104
  also \cite{isabelle-ref}).  Thus the output behavior may be modified
wenzelm@27052
   105
  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
wenzelm@27052
   106
  proof state with mathematical symbols and special characters
wenzelm@27052
   107
  represented in {\LaTeX} source, according to the Isabelle style
wenzelm@27052
   108
  \cite{isabelle-sys}.
wenzelm@27052
   109
wenzelm@27052
   110
  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
wenzelm@27052
   111
  systematic way to include formal items into the printed text
wenzelm@27052
   112
  document.%
wenzelm@27052
   113
\end{isamarkuptext}%
wenzelm@27052
   114
\isamarkuptrue%
wenzelm@27052
   115
%
wenzelm@27052
   116
\isamarkupsection{Inspecting the context%
wenzelm@27052
   117
}
wenzelm@27052
   118
\isamarkuptrue%
wenzelm@27052
   119
%
wenzelm@27052
   120
\begin{isamarkuptext}%
wenzelm@27052
   121
\begin{matharray}{rcl}
wenzelm@27052
   122
    \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} \\
wenzelm@27052
   123
    \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} \\
wenzelm@27052
   124
    \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} \\
wenzelm@27052
   125
    \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} \\
wenzelm@27052
   126
    \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} \\
wenzelm@27052
   127
    \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} \\
wenzelm@27052
   128
    \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} \\
wenzelm@27052
   129
    \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} \\
wenzelm@27052
   130
    \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} \\
wenzelm@27052
   131
    \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} \\
wenzelm@27052
   132
  \end{matharray}
wenzelm@27052
   133
wenzelm@27052
   134
  \begin{rail}
wenzelm@27052
   135
    'print\_theory' ( '!'?)
wenzelm@27052
   136
    ;
wenzelm@27052
   137
wenzelm@27052
   138
    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
wenzelm@27052
   139
    ;
wenzelm@27052
   140
    criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
wenzelm@27052
   141
      'simp' ':' term | term)
wenzelm@27052
   142
    ;
wenzelm@27052
   143
    'thm\_deps' thmrefs
wenzelm@27052
   144
    ;
wenzelm@27052
   145
  \end{rail}
wenzelm@27052
   146
wenzelm@27052
   147
  These commands print certain parts of the theory and proof context.
wenzelm@27052
   148
  Note that there are some further ones available, such as for the set
wenzelm@27052
   149
  of rules declared for simplifications.
wenzelm@27052
   150
wenzelm@27052
   151
  \begin{descr}
wenzelm@27052
   152
  
wenzelm@27052
   153
  \item [\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory
wenzelm@27052
   154
  syntax, including keywords and command.
wenzelm@27052
   155
  
wenzelm@27052
   156
  \item [\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of
wenzelm@27052
   157
  the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra
wenzelm@27052
   158
  verbosity.
wenzelm@27052
   159
wenzelm@27052
   160
  \item [\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types
wenzelm@27052
   161
  and terms, depending on the current context.  The output can be very
wenzelm@27052
   162
  verbose, including grammar tables and syntax translation rules.  See
wenzelm@27052
   163
  \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
wenzelm@27052
   164
  inner syntax.
wenzelm@27052
   165
  
wenzelm@27052
   166
  \item [\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods
wenzelm@27052
   167
  available in the current theory context.
wenzelm@27052
   168
  
wenzelm@27052
   169
  \item [\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes
wenzelm@27052
   170
  available in the current theory context.
wenzelm@27052
   171
  
wenzelm@27052
   172
  \item [\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from
wenzelm@27052
   173
  the last command.
wenzelm@27052
   174
  
wenzelm@27052
   175
  \item [\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts
wenzelm@27052
   176
  from the theory or proof context matching all of given search
wenzelm@27052
   177
  criteria.  The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems
wenzelm@27052
   178
  whose fully qualified name matches pattern \isa{p}, which may
wenzelm@27052
   179
  contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards.  The criteria \isa{intro},
wenzelm@27052
   180
  \isa{elim}, and \isa{dest} select theorems that match the
wenzelm@27052
   181
  current goal as introduction, elimination or destruction rules,
wenzelm@27052
   182
  respectively.  The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite
wenzelm@27052
   183
  rules whose left-hand side matches the given term.  The criterion
wenzelm@27052
   184
  term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
wenzelm@27052
   185
  ``\isa{{\isacharunderscore}}'', schematic variables, and type constraints.
wenzelm@27052
   186
  
wenzelm@27052
   187
  Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that
wenzelm@27052
   188
  do \emph{not} match. Note that giving the empty list of criteria
wenzelm@27052
   189
  yields \emph{all} currently known facts.  An optional limit for the
wenzelm@27052
   190
  number of printed facts may be given; the default is 40.  By
wenzelm@27052
   191
  default, duplicates are removed from the search result. Use
wenzelm@27052
   192
  \isa{with{\isacharunderscore}dups} to display duplicates.
wenzelm@27052
   193
  
wenzelm@27052
   194
  \item [\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
wenzelm@27052
   195
  visualizes dependencies of facts, using Isabelle's graph browser
wenzelm@27052
   196
  tool (see also \cite{isabelle-sys}).
wenzelm@27052
   197
  
wenzelm@27052
   198
  \item [\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the
wenzelm@27052
   199
  current context, both named and unnamed ones.
wenzelm@27052
   200
  
wenzelm@27052
   201
  \item [\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations
wenzelm@27052
   202
  present in the context.
wenzelm@27052
   203
wenzelm@27052
   204
  \end{descr}%
wenzelm@27052
   205
\end{isamarkuptext}%
wenzelm@27052
   206
\isamarkuptrue%
wenzelm@27052
   207
%
wenzelm@27052
   208
\isamarkupsection{History commands \label{sec:history}%
wenzelm@27052
   209
}
wenzelm@27052
   210
\isamarkuptrue%
wenzelm@27052
   211
%
wenzelm@27052
   212
\begin{isamarkuptext}%
wenzelm@27052
   213
\begin{matharray}{rcl}
wenzelm@27052
   214
    \indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
wenzelm@27052
   215
    \indexdef{}{command}{redo}\hypertarget{command.redo}{\hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
wenzelm@27052
   216
    \indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
wenzelm@27052
   217
  \end{matharray}
wenzelm@27052
   218
wenzelm@27052
   219
  The Isabelle/Isar top-level maintains a two-stage history, for
wenzelm@27052
   220
  theory and proof state transformation.  Basically, any command can
wenzelm@27052
   221
  be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic
wenzelm@27052
   222
  elements.  Its effect may be revoked via \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, unless
wenzelm@27052
   223
  the corresponding \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} step has crossed the beginning
wenzelm@27052
   224
  of a proof or theory.  The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts the
wenzelm@27052
   225
  current history node altogether, discontinuing a proof or even the
wenzelm@27052
   226
  whole theory.  This operation is \emph{not} undo-able.
wenzelm@27052
   227
wenzelm@27052
   228
  \begin{warn}
wenzelm@27052
   229
    History commands should never be used with user interfaces such as
wenzelm@27052
   230
    Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
wenzelm@27052
   231
    care of stepping forth and back itself.  Interfering by manual
wenzelm@27052
   232
    \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}
wenzelm@27052
   233
    commands would quickly result in utter confusion.
wenzelm@27052
   234
  \end{warn}%
wenzelm@27052
   235
\end{isamarkuptext}%
wenzelm@27052
   236
\isamarkuptrue%
wenzelm@27052
   237
%
wenzelm@27054
   238
\isamarkupsection{System commands%
wenzelm@27052
   239
}
wenzelm@27052
   240
\isamarkuptrue%
wenzelm@27052
   241
%
wenzelm@27052
   242
\begin{isamarkuptext}%
wenzelm@27052
   243
\begin{matharray}{rcl}
wenzelm@27052
   244
    \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
wenzelm@27052
   245
    \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
wenzelm@27052
   246
    \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} \\
wenzelm@27052
   247
  \end{matharray}
wenzelm@27052
   248
wenzelm@27052
   249
  \begin{rail}
wenzelm@27052
   250
    ('cd' | 'use\_thy' | 'update\_thy') name
wenzelm@27052
   251
    ;
wenzelm@27052
   252
  \end{rail}
wenzelm@27052
   253
wenzelm@27052
   254
  \begin{descr}
wenzelm@27052
   255
wenzelm@27052
   256
  \item [\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path}] changes the current directory
wenzelm@27052
   257
  of the Isabelle process.
wenzelm@27052
   258
wenzelm@27052
   259
  \item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory.
wenzelm@27052
   260
wenzelm@27052
   261
  \item [\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}.
wenzelm@27052
   262
  These system commands are scarcely used when working interactively,
wenzelm@27052
   263
  since loading of theories is done automatically as required.
wenzelm@27052
   264
wenzelm@27052
   265
  \end{descr}%
wenzelm@27052
   266
\end{isamarkuptext}%
wenzelm@27052
   267
\isamarkuptrue%
wenzelm@27052
   268
%
wenzelm@27052
   269
\isadelimtheory
wenzelm@27052
   270
%
wenzelm@27052
   271
\endisadelimtheory
wenzelm@27052
   272
%
wenzelm@27052
   273
\isatagtheory
wenzelm@27052
   274
\isacommand{end}\isamarkupfalse%
wenzelm@27052
   275
%
wenzelm@27052
   276
\endisatagtheory
wenzelm@27052
   277
{\isafoldtheory}%
wenzelm@27052
   278
%
wenzelm@27052
   279
\isadelimtheory
wenzelm@27052
   280
%
wenzelm@27052
   281
\endisadelimtheory
wenzelm@27052
   282
\isanewline
wenzelm@27052
   283
\end{isabellebody}%
wenzelm@27052
   284
%%% Local Variables:
wenzelm@27052
   285
%%% mode: latex
wenzelm@27052
   286
%%% TeX-master: "root"
wenzelm@27052
   287
%%% End: