61 \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
61 \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
62 \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
62 \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
63 \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
63 \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
64 \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
64 \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
65 \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
65 \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
66 \indexdef{}{command}{text\_raw}\hypertarget{command.text_raw}{\hyperlink{command.text_raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
66 \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isarkeep{local{\dsh}theory} \\ |
67 \end{matharray} |
67 \end{matharray} |
68 |
68 |
69 Apart from formal comments (see \secref{sec:comments}), markup |
69 Apart from formal comments (see \secref{sec:comments}), markup |
70 commands provide a structured way to insert text into the document |
70 commands provide a structured way to insert text into the document |
71 generated from a theory (see \cite{isabelle-sys} for more |
71 generated from a theory (see \cite{isabelle-sys} for more |
83 \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 |
83 \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 |
84 section headings. |
84 section headings. |
85 |
85 |
86 \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}] specifies paragraphs of plain text. |
86 \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}] specifies paragraphs of plain text. |
87 |
87 |
88 \item [\hyperlink{command.text_raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}] inserts {\LaTeX} source into the |
88 \item [\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}] inserts {\LaTeX} source into the |
89 output, without additional markup. Thus the full range of document |
89 output, without additional markup. Thus the full range of document |
90 manipulations becomes available. |
90 manipulations becomes available. |
91 |
91 |
92 \end{descr} |
92 \end{descr} |
93 |
93 |
94 The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for |
94 The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for |
95 \hyperlink{command.text_raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities |
95 \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities |
96 (``antiquotations'', see also \secref{sec:antiq}). These are |
96 (``antiquotations'', see also \secref{sec:antiq}). These are |
97 interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}. |
97 interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}. |
98 |
98 |
99 Any of these markup elements corresponds to a {\LaTeX} command with |
99 Any of these markup elements corresponds to a {\LaTeX} command with |
100 the name prefixed by \verb|\isamarkup|. For the sectioning |
100 the name prefixed by \verb|\isamarkup|. For the sectioning |
101 commands this is a plain macro with a single argument, e.g.\ |
101 commands this is a plain macro with a single argument, e.g.\ |
102 \verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for |
102 \verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for |
103 \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}. The \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} markup results in a |
103 \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}. The \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} markup results in a |
104 {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text_raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} |
104 {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} |
105 causes the text to be inserted directly into the {\LaTeX} source. |
105 causes the text to be inserted directly into the {\LaTeX} source. |
106 |
106 |
107 \medskip Additional markup commands are available for proofs (see |
107 \medskip Additional markup commands are available for proofs (see |
108 \secref{sec:markup-prf}). Also note that the \indexref{}{command}{header}\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration (see \secref{sec:begin-thy}) admits to insert |
108 \secref{sec:markup-prf}). Also note that the \indexref{}{command}{header}\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration (see \secref{sec:begin-thy}) admits to insert |
109 section markup just preceding the actual theory definition.% |
109 section markup just preceding the actual theory definition.% |
117 \begin{isamarkuptext}% |
117 \begin{isamarkuptext}% |
118 \begin{matharray}{rcll} |
118 \begin{matharray}{rcll} |
119 \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\ |
119 \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\ |
120 \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\ |
120 \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\ |
121 \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\ |
121 \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\ |
122 \indexdef{}{command}{class\_deps}\hypertarget{command.class_deps}{\hyperlink{command.class_deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\ |
122 \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\ |
123 \end{matharray} |
123 \end{matharray} |
124 |
124 |
125 \begin{rail} |
125 \begin{rail} |
126 'classes' (classdecl +) |
126 'classes' (classdecl +) |
127 ; |
127 ; |
144 \item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{s} the |
144 \item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{s} the |
145 new default sort for any type variables given without sort |
145 new default sort for any type variables given without sort |
146 constraints. Usually, the default sort would be only changed when |
146 constraints. Usually, the default sort would be only changed when |
147 defining a new object-logic. |
147 defining a new object-logic. |
148 |
148 |
149 \item [\hyperlink{command.class_deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation, |
149 \item [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation, |
150 using Isabelle's graph browser tool (see also \cite{isabelle-sys}). |
150 using Isabelle's graph browser tool (see also \cite{isabelle-sys}). |
151 |
151 |
152 \end{descr}% |
152 \end{descr}% |
153 \end{isamarkuptext}% |
153 \end{isamarkuptext}% |
154 \isamarkuptrue% |
154 \isamarkuptrue% |
313 \isamarkuptrue% |
313 \isamarkuptrue% |
314 % |
314 % |
315 \begin{isamarkuptext}% |
315 \begin{isamarkuptext}% |
316 \begin{matharray}{rcl} |
316 \begin{matharray}{rcl} |
317 \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\ |
317 \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\ |
318 \indexdef{}{command}{no\_syntax}\hypertarget{command.no_syntax}{\hyperlink{command.no_syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\ |
318 \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\ |
319 \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\ |
319 \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\ |
320 \indexdef{}{command}{no\_translations}\hypertarget{command.no_translations}{\hyperlink{command.no_translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\ |
320 \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\ |
321 \end{matharray} |
321 \end{matharray} |
322 |
322 |
323 \begin{rail} |
323 \begin{rail} |
324 ('syntax' | 'no\_syntax') mode? (constdecl +) |
324 ('syntax' | 'no\_syntax') mode? (constdecl +) |
325 ; |
325 ; |
340 Isabelle's inner syntax may be augmented in arbitrary ways, |
340 Isabelle's inner syntax may be augmented in arbitrary ways, |
341 independently of the logic. The \isa{mode} argument refers to the |
341 independently of the logic. The \isa{mode} argument refers to the |
342 print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the |
342 print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the |
343 input and output grammar. |
343 input and output grammar. |
344 |
344 |
345 \item [\hyperlink{command.no_syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes |
345 \item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes |
346 grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above. |
346 grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above. |
347 |
347 |
348 \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic |
348 \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic |
349 translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}), |
349 translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}), |
350 parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}). |
350 parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}). |
351 Translation patterns may be prefixed by the syntactic category to be |
351 Translation patterns may be prefixed by the syntactic category to be |
352 used for parsing; the default is \isa{logic}. |
352 used for parsing; the default is \isa{logic}. |
353 |
353 |
354 \item [\hyperlink{command.no_translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic |
354 \item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic |
355 translation rules, which are interpreted in the same manner as for |
355 translation rules, which are interpreted in the same manner as for |
356 \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above. |
356 \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above. |
357 |
357 |
358 \end{descr}% |
358 \end{descr}% |
359 \end{isamarkuptext}% |
359 \end{isamarkuptext}% |
454 % |
454 % |
455 \begin{isamarkuptext}% |
455 \begin{isamarkuptext}% |
456 \begin{matharray}{rcl} |
456 \begin{matharray}{rcl} |
457 \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\ |
457 \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\ |
458 \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\ |
458 \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\ |
459 \indexdef{}{command}{ML\_val}\hypertarget{command.ML_val}{\hyperlink{command.ML_val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\ |
459 \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\ |
460 \indexdef{}{command}{ML\_command}\hypertarget{command.ML_command}{\hyperlink{command.ML_command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\ |
460 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\ |
461 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\ |
461 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\ |
462 \indexdef{}{command}{method\_setup}\hypertarget{command.method_setup}{\hyperlink{command.method_setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\ |
462 \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\ |
463 \end{matharray} |
463 \end{matharray} |
464 |
464 |
465 \begin{rail} |
465 \begin{rail} |
466 'use' name |
466 'use' name |
467 ; |
467 ; |
479 the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory |
479 the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory |
480 header (see also \secref{sec:begin-thy}). |
480 header (see also \secref{sec:begin-thy}). |
481 |
481 |
482 \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}. |
482 \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}. |
483 |
483 |
484 \item [\hyperlink{command.ML_val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML_command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are |
484 \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are |
485 diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context |
485 diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context |
486 may not be updated. \hyperlink{command.ML_val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced |
486 may not be updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced |
487 at the ML toplevel, but \hyperlink{command.ML_command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent. |
487 at the ML toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent. |
488 |
488 |
489 \item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory |
489 \item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory |
490 context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression |
490 context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression |
491 of type \verb|"theory -> theory"|. This enables to initialize |
491 of type \verb|"theory -> theory"|. This enables to initialize |
492 any object-logic specific tools and packages written in ML, for |
492 any object-logic specific tools and packages written in ML, for |
493 example. |
493 example. |
494 |
494 |
495 \item [\hyperlink{command.method_setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}] |
495 \item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}] |
496 defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline% |
496 defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline% |
497 \verb| Proof.context -> Proof.method"|. Parsing concrete method syntax |
497 \verb| Proof.context -> Proof.method"|. Parsing concrete method syntax |
498 from \verb|Args.src| input can be quite tedious in general. The |
498 from \verb|Args.src| input can be quite tedious in general. The |
499 following simple examples are for methods without any explicit |
499 following simple examples are for methods without any explicit |
500 arguments, or a list of theorems, respectively. |
500 arguments, or a list of theorems, respectively. |
524 } |
524 } |
525 \isamarkuptrue% |
525 \isamarkuptrue% |
526 % |
526 % |
527 \begin{isamarkuptext}% |
527 \begin{isamarkuptext}% |
528 \begin{matharray}{rcl} |
528 \begin{matharray}{rcl} |
529 \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse_ast_translation}{\hyperlink{command.parse_ast_translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
529 \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
530 \indexdef{}{command}{parse\_translation}\hypertarget{command.parse_translation}{\hyperlink{command.parse_translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
530 \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
531 \indexdef{}{command}{print\_translation}\hypertarget{command.print_translation}{\hyperlink{command.print_translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
531 \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
532 \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed_print_translation}{\hyperlink{command.typed_print_translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
532 \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
533 \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print_ast_translation}{\hyperlink{command.print_ast_translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
533 \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
534 \indexdef{}{command}{token\_translation}\hypertarget{command.token_translation}{\hyperlink{command.token_translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
534 \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ |
535 \end{matharray} |
535 \end{matharray} |
536 |
536 |
537 \begin{rail} |
537 \begin{rail} |
538 ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | |
538 ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | |
539 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text |
539 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text |
632 \begin{matharray}{rcl} |
632 \begin{matharray}{rcl} |
633 \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isartrans{proof}{proof} \\ |
633 \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isartrans{proof}{proof} \\ |
634 \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isartrans{proof}{proof} \\ |
634 \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isartrans{proof}{proof} \\ |
635 \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isartrans{proof}{proof} \\ |
635 \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isartrans{proof}{proof} \\ |
636 \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isartrans{proof}{proof} \\ |
636 \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isartrans{proof}{proof} \\ |
637 \indexdef{}{command}{txt\_raw}\hypertarget{command.txt_raw}{\hyperlink{command.txt_raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isartrans{proof}{proof} \\ |
637 \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isartrans{proof}{proof} \\ |
638 \end{matharray} |
638 \end{matharray} |
639 |
639 |
640 These markup commands for proof mode closely correspond to the ones |
640 These markup commands for proof mode closely correspond to the ones |
641 of theory mode (see \S\ref{sec:markup-thy}). |
641 of theory mode (see \S\ref{sec:markup-thy}). |
642 |
642 |
661 \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
661 \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
662 \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
662 \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
663 \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
663 \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
664 \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
664 \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
665 \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
665 \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
666 \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} \\ |
666 \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} \\ |
667 \end{matharray} |
667 \end{matharray} |
668 |
668 |
669 These diagnostic commands assist interactive development. Note that |
669 These diagnostic commands assist interactive development. Note that |
670 \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} does not apply here, the theory or proof |
670 \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} does not apply here, the theory or proof |
671 configuration is not changed. |
671 configuration is not changed. |
717 current proof state (if present), or of the given theorems. Note |
717 current proof state (if present), or of the given theorems. Note |
718 that this requires proof terms to be switched on for the current |
718 that this requires proof terms to be switched on for the current |
719 object logic (see the ``Proof terms'' section of the Isabelle |
719 object logic (see the ``Proof terms'' section of the Isabelle |
720 reference manual for information on how to do this). |
720 reference manual for information on how to do this). |
721 |
721 |
722 \item [\hyperlink{command.full_prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays |
722 \item [\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays |
723 the full proof term, i.e.\ also displays information omitted in the |
723 the full proof term, i.e.\ also displays information omitted in the |
724 compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders |
724 compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders |
725 there. |
725 there. |
726 |
726 |
727 \end{descr} |
727 \end{descr} |
744 } |
744 } |
745 \isamarkuptrue% |
745 \isamarkuptrue% |
746 % |
746 % |
747 \begin{isamarkuptext}% |
747 \begin{isamarkuptext}% |
748 \begin{matharray}{rcl} |
748 \begin{matharray}{rcl} |
749 \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} \\ |
749 \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} \\ |
750 \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} \\ |
750 \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} \\ |
751 \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} \\ |
751 \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} \\ |
752 \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} \\ |
752 \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} \\ |
753 \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} \\ |
753 \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} \\ |
754 \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} \\ |
754 \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} \\ |
755 \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} \\ |
755 \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} \\ |
756 \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} \\ |
756 \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} \\ |
757 \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} \\ |
757 \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} \\ |
758 \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} \\ |
758 \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} \\ |
759 \end{matharray} |
759 \end{matharray} |
760 |
760 |
761 \begin{rail} |
761 \begin{rail} |
762 'print\_theory' ( '!'?) |
762 'print\_theory' ( '!'?) |
763 ; |
763 ; |
775 Note that there are some further ones available, such as for the set |
775 Note that there are some further ones available, such as for the set |
776 of rules declared for simplifications. |
776 of rules declared for simplifications. |
777 |
777 |
778 \begin{descr} |
778 \begin{descr} |
779 |
779 |
780 \item [\hyperlink{command.print_commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory |
780 \item [\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory |
781 syntax, including keywords and command. |
781 syntax, including keywords and command. |
782 |
782 |
783 \item [\hyperlink{command.print_theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of |
783 \item [\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of |
784 the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra |
784 the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra |
785 verbosity. |
785 verbosity. |
786 |
786 |
787 \item [\hyperlink{command.print_syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types |
787 \item [\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types |
788 and terms, depending on the current context. The output can be very |
788 and terms, depending on the current context. The output can be very |
789 verbose, including grammar tables and syntax translation rules. See |
789 verbose, including grammar tables and syntax translation rules. See |
790 \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's |
790 \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's |
791 inner syntax. |
791 inner syntax. |
792 |
792 |
793 \item [\hyperlink{command.print_methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods |
793 \item [\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods |
794 available in the current theory context. |
794 available in the current theory context. |
795 |
795 |
796 \item [\hyperlink{command.print_attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes |
796 \item [\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes |
797 available in the current theory context. |
797 available in the current theory context. |
798 |
798 |
799 \item [\hyperlink{command.print_theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from |
799 \item [\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from |
800 the last command. |
800 the last command. |
801 |
801 |
802 \item [\hyperlink{command.find_theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts |
802 \item [\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts |
803 from the theory or proof context matching all of given search |
803 from the theory or proof context matching all of given search |
804 criteria. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems |
804 criteria. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems |
805 whose fully qualified name matches pattern \isa{p}, which may |
805 whose fully qualified name matches pattern \isa{p}, which may |
806 contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards. The criteria \isa{intro}, |
806 contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards. The criteria \isa{intro}, |
807 \isa{elim}, and \isa{dest} select theorems that match the |
807 \isa{elim}, and \isa{dest} select theorems that match the |
816 yields \emph{all} currently known facts. An optional limit for the |
816 yields \emph{all} currently known facts. An optional limit for the |
817 number of printed facts may be given; the default is 40. By |
817 number of printed facts may be given; the default is 40. By |
818 default, duplicates are removed from the search result. Use |
818 default, duplicates are removed from the search result. Use |
819 \isa{with{\isacharunderscore}dups} to display duplicates. |
819 \isa{with{\isacharunderscore}dups} to display duplicates. |
820 |
820 |
821 \item [\hyperlink{command.thm_deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] |
821 \item [\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] |
822 visualizes dependencies of facts, using Isabelle's graph browser |
822 visualizes dependencies of facts, using Isabelle's graph browser |
823 tool (see also \cite{isabelle-sys}). |
823 tool (see also \cite{isabelle-sys}). |
824 |
824 |
825 \item [\hyperlink{command.print_facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the |
825 \item [\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the |
826 current context, both named and unnamed ones. |
826 current context, both named and unnamed ones. |
827 |
827 |
828 \item [\hyperlink{command.print_binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations |
828 \item [\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations |
829 present in the context. |
829 present in the context. |
830 |
830 |
831 \end{descr}% |
831 \end{descr}% |
832 \end{isamarkuptext}% |
832 \end{isamarkuptext}% |
833 \isamarkuptrue% |
833 \isamarkuptrue% |
868 % |
868 % |
869 \begin{isamarkuptext}% |
869 \begin{isamarkuptext}% |
870 \begin{matharray}{rcl} |
870 \begin{matharray}{rcl} |
871 \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
871 \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
872 \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
872 \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
873 \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} \\ |
873 \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} \\ |
874 \indexdef{}{command}{display\_drafts}\hypertarget{command.display_drafts}{\hyperlink{command.display_drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
874 \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
875 \indexdef{}{command}{print\_drafts}\hypertarget{command.print_drafts}{\hyperlink{command.print_drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
875 \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
876 \end{matharray} |
876 \end{matharray} |
877 |
877 |
878 \begin{rail} |
878 \begin{rail} |
879 ('cd' | 'use\_thy' | 'update\_thy') name |
879 ('cd' | 'use\_thy' | 'update\_thy') name |
880 ; |
880 ; |
887 \item [\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path}] changes the current directory |
887 \item [\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path}] changes the current directory |
888 of the Isabelle process. |
888 of the Isabelle process. |
889 |
889 |
890 \item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory. |
890 \item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory. |
891 |
891 |
892 \item [\hyperlink{command.use_thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}. |
892 \item [\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}. |
893 These system commands are scarcely used when working interactively, |
893 These system commands are scarcely used when working interactively, |
894 since loading of theories is done automatically as required. |
894 since loading of theories is done automatically as required. |
895 |
895 |
896 \item [\hyperlink{command.display_drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print_drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{paths}] perform simple output of a given list |
896 \item [\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{paths}] perform simple output of a given list |
897 of raw source files. Only those symbols that do not require |
897 of raw source files. Only those symbols that do not require |
898 additional {\LaTeX} packages are displayed properly, everything else |
898 additional {\LaTeX} packages are displayed properly, everything else |
899 is left verbatim. |
899 is left verbatim. |
900 |
900 |
901 \end{descr}% |
901 \end{descr}% |