wneuper/isa: doc-src/IsarRef/Thy/document/Misc.tex@012a887997f3

1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Misc}%

4 %

     5 \isadelimtheory

6 %

     7 \endisadelimtheory

8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

    11 \ Misc\isanewline

    12 \isakeyword{imports}\ Base\ Main\isanewline

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

    21 \isamarkupchapter{Other commands%

    22 }

    23 \isamarkuptrue%

    24 %

    25 \isamarkupsection{Inspecting the context%

    26 }

    27 \isamarkuptrue%

    28 %

    29 \begin{isamarkuptext}%

    30 \begin{matharray}{rcl}

    31     \indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}commands}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    32     \indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    33     \indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}methods}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    34     \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}attributes}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    35     \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    36     \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    37     \indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    38     \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    39     \indexdef{}{command}{unused\_thms}\hypertarget{command.unused-thms}{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    40     \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    41     \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}binds}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

    42   \end{matharray}

    44   \begin{railoutput}

    45 \rail@begin{2}{}

    46 \rail@bar

    47 \rail@term{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}[]

    48 \rail@nextbar{1}

    49 \rail@term{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]

    50 \rail@endbar

    51 \rail@bar

    52 \rail@nextbar{1}

    53 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]

    54 \rail@endbar

    55 \rail@end

    56 \rail@begin{6}{}

    57 \rail@term{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]

    58 \rail@bar

    59 \rail@nextbar{1}

    60 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

    61 \rail@bar

    62 \rail@nextbar{2}

    63 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

    64 \rail@endbar

    65 \rail@bar

    66 \rail@nextbar{2}

    67 \rail@term{\isa{with{\isaliteral{5F}{\isacharunderscore}}dups}}[]

    68 \rail@endbar

    69 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

    70 \rail@endbar

    71 \rail@cr{4}

    72 \rail@plus

    73 \rail@nextplus{5}

    74 \rail@cnont{\isa{thmcriterion}}[]

    75 \rail@endplus

    76 \rail@end

    77 \rail@begin{7}{\isa{thmcriterion}}

    78 \rail@bar

    79 \rail@nextbar{1}

    80 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

    81 \rail@endbar

    82 \rail@bar

    83 \rail@term{\isa{name}}[]

    84 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

    85 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

    86 \rail@nextbar{1}

    87 \rail@term{\isa{intro}}[]

    88 \rail@nextbar{2}

    89 \rail@term{\isa{elim}}[]

    90 \rail@nextbar{3}

    91 \rail@term{\isa{dest}}[]

    92 \rail@nextbar{4}

    93 \rail@term{\isa{solves}}[]

    94 \rail@nextbar{5}

    95 \rail@term{\isa{simp}}[]

    96 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

    97 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

    98 \rail@nextbar{6}

    99 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

   100 \rail@endbar

   101 \rail@end

   102 \rail@begin{2}{}

   103 \rail@term{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}[]

   104 \rail@plus

   105 \rail@nextplus{1}

   106 \rail@cnont{\isa{constcriterion}}[]

   107 \rail@endplus

   108 \rail@end

   109 \rail@begin{3}{\isa{constcriterion}}

   110 \rail@bar

   111 \rail@nextbar{1}

   112 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

   113 \rail@endbar

   114 \rail@bar

   115 \rail@term{\isa{name}}[]

   116 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

   117 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   118 \rail@nextbar{1}

   119 \rail@term{\isa{strict}}[]

   120 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

   121 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

   122 \rail@nextbar{2}

   123 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

   124 \rail@endbar

   125 \rail@end

   126 \rail@begin{1}{}

   127 \rail@term{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]

   128 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

   129 \rail@end

   130 \rail@begin{3}{}

   131 \rail@term{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]

   132 \rail@bar

   133 \rail@nextbar{1}

   134 \rail@plus

   135 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   136 \rail@nextplus{2}

   137 \rail@endplus

   138 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

   139 \rail@plus

   140 \rail@nextplus{2}

   141 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   142 \rail@endplus

   143 \rail@endbar

   144 \rail@end

   145 \end{railoutput}

   148   These commands print certain parts of the theory and proof context.

   149   Note that there are some further ones available, such as for the set

   150   of rules declared for simplifications.

   152   \begin{description}

   154   \item \hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}commands}}}} prints Isabelle's outer theory

   155   syntax, including keywords and command.

   157   \item \hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}} prints the main logical content of

   158   the theory context; the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' option indicates extra

   159   verbosity.

   161   \item \hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}methods}}}} prints all proof methods

   162   available in the current theory context.

   164   \item \hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}attributes}}}} prints all attributes

   165   available in the current theory context.

   167   \item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}} prints theorems resulting from the

   168   last command; the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' option indicates extra verbosity.

   170   \item \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}~\isa{criteria} retrieves facts

   171   from the theory or proof context matching all of given search

   172   criteria.  The criterion \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ p{\isaliteral{22}{\isachardoublequote}}} selects all theorems

   173   whose fully qualified name matches pattern \isa{p}, which may

   174   contain ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}'' wildcards.  The criteria \isa{intro},

   175   \isa{elim}, and \isa{dest} select theorems that match the

   176   current goal as introduction, elimination or destruction rules,

   177   respectively.  The criterion \isa{{\isaliteral{22}{\isachardoublequote}}solves{\isaliteral{22}{\isachardoublequote}}} returns all rules

   178   that would directly solve the current goal.  The criterion

   179   \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}\ t{\isaliteral{22}{\isachardoublequote}}} selects all rewrite rules whose left-hand side

   180   matches the given term.  The criterion term \isa{t} selects all

   181   theorems that contain the pattern \isa{t} -- as usual, patterns

   182   may contain occurrences of the dummy ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'', schematic

   183   variables, and type constraints.

   185   Criteria can be preceded by ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' to select theorems that

   186   do \emph{not} match. Note that giving the empty list of criteria

   187   yields \emph{all} currently known facts.  An optional limit for the

   188   number of printed facts may be given; the default is 40.  By

   189   default, duplicates are removed from the search result. Use

   190   \isa{with{\isaliteral{5F}{\isacharunderscore}}dups} to display duplicates.

   192   \item \hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}~\isa{criteria} prints all constants

   193   whose type meets all of the given criteria. The criterion \isa{{\isaliteral{22}{\isachardoublequote}}strict{\isaliteral{3A}{\isacharcolon}}\ ty{\isaliteral{22}{\isachardoublequote}}} is met by any type that matches the type pattern

   194   \isa{ty}.  Patterns may contain both the dummy type ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''

   195   and sort constraints. The criterion \isa{ty} is similar, but it

   196   also matches against subtypes. The criterion \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ p{\isaliteral{22}{\isachardoublequote}}} and

   197   the prefix ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' function as described for \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}.

   199   \item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}

   200   visualizes dependencies of facts, using Isabelle's graph browser

   201   tool (see also \cite{isabelle-sys}).

   203   \item \hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m\ {\isaliteral{2D}{\isacharminus}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}

   204   displays all unused theorems in theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}

   205   or their parents, but not in \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{22}{\isachardoublequote}}} or their parents.

   206   If \isa{n} is \isa{{\isadigit{0}}}, the end of the range of theories

   207   defaults to the current theory. If no range is specified,

   208   only the unused theorems in the current theory are displayed.

   210   \item \hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}} prints all local facts of the

   211   current context, both named and unnamed ones.

   213   \item \hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}binds}}}} prints all term abbreviations

   214   present in the context.

   216   \end{description}%

   217 \end{isamarkuptext}%

   218 \isamarkuptrue%

   219 %

   220 \isamarkupsection{System commands%

   221 }

   222 \isamarkuptrue%

   223 %

   224 \begin{isamarkuptext}%

   225 \begin{matharray}{rcl}

   226     \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   227     \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   228     \indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   229   \end{matharray}

   231   \begin{railoutput}

   232 \rail@begin{2}{}

   233 \rail@bar

   234 \rail@term{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}[]

   235 \rail@nextbar{1}

   236 \rail@term{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}}[]

   237 \rail@endbar

   238 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   239 \rail@end

   240 \end{railoutput}

   243   \begin{description}

   245   \item \hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path} changes the current directory

   246   of the Isabelle process.

   248   \item \hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}} prints the current working directory.

   250   \item \hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}~\isa{A} preload theory \isa{A}.

   251   These system commands are scarcely used when working interactively,

   252   since loading of theories is done automatically as required.

   254   \end{description}

   256   %FIXME proper place (!?)

   257   Isabelle file specification may contain path variables (e.g.\

   258   \verb|$ISABELLE_HOME|) that are expanded accordingly.  Note

   259   that \verb|~| abbreviates \verb|$USER_HOME|, and

   260   \verb|~~| abbreviates \verb|$ISABELLE_HOME|.  The

   261   general syntax for path specifications follows POSIX conventions.%

   262 \end{isamarkuptext}%

   263 \isamarkuptrue%

   264 %

   265 \isadelimtheory

   266 %

   267 \endisadelimtheory

   268 %

   269 \isatagtheory

   270 \isacommand{end}\isamarkupfalse%

   271 %

   272 \endisatagtheory

   273 {\isafoldtheory}%

   274 %

   275 \isadelimtheory

   276 %

   277 \endisadelimtheory

   278 \isanewline

   279 \end{isabellebody}%

   280 %%% Local Variables:

   281 %%% mode: latex

   282 %%% TeX-master: "root"

   283 %%% End:

author	wenzelm
	Sun, 22 Apr 2012 14:30:18 +0200
changeset 48538	012a887997f3
parent 47310	ddf7f79abdac
permissions	-rw-r--r--