--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 13 21:50:57 2008 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 13 21:52:09 2008 +0100
@@ -12,32 +12,30 @@
text {*
\begin{matharray}{rcl}
- @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
- @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
\end{matharray}
These diagnostic commands assist interactive development by printing
internal logical entities in a human-readable fashion.
\begin{rail}
- 'pr' modes? nat? (',' nat)?
- ;
- 'thm' modes? thmrefs
+ 'typ' modes? type
;
'term' modes? term
;
'prop' modes? prop
;
- 'typ' modes? type
+ 'thm' modes? thmrefs
;
- 'prf' modes? thmrefs?
+ ( 'prf' | 'full\_prf' ) modes? thmrefs?
;
- 'full\_prf' modes? thmrefs?
+ 'pr' modes? nat? (',' nat)?
;
modes: '(' (name + ) ')'
@@ -46,11 +44,14 @@
\begin{description}
- \item @{command "pr"}~@{text "goals, prems"} prints the current
- proof state (if present), including the proof context, current facts
- and goals. The optional limit arguments affect the number of goals
- and premises to be displayed, which is initially 10 for both.
- Omitting limit values leaves the current setting unchanged.
+ \item @{command "typ"}~@{text \<tau>} reads and prints types of the
+ meta-logic according to the current theory or proof context.
+
+ \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
+ read, type-check and print terms or propositions according to the
+ current theory or proof context; the inferred type of @{text t} is
+ output as well. Note that these commands are also useful in
+ inspecting the current environment of term abbreviations.
\item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
theorems from the current theory or proof context. Note that any
@@ -59,15 +60,6 @@
result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
\<dots>, a\<^sub>n"} do not have any permanent effect.
- \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
- read, type-check and print terms or propositions according to the
- current theory or proof context; the inferred type of @{text t} is
- output as well. Note that these commands are also useful in
- inspecting the current environment of term abbreviations.
-
- \item @{command "typ"}~@{text \<tau>} reads and prints types of the
- meta-logic according to the current theory or proof context.
-
\item @{command "prf"} displays the (compact) proof term of the
current proof state (if present), or of the given theorems. Note
that this requires proof terms to be switched on for the current
@@ -79,6 +71,12 @@
compact proof term, which is denoted by ``@{text _}'' placeholders
there.
+ \item @{command "pr"}~@{text "goals, prems"} prints the current
+ proof state (if present), including the proof context, current facts
+ and goals. The optional limit arguments affect the number of goals
+ and premises to be displayed, which is initially 10 for both.
+ Omitting limit values leaves the current setting unchanged.
+
\end{description}
All of the diagnostic commands above admit a list of @{text modes}
@@ -355,7 +353,7 @@
*}
-section {* Additional term notation *}
+section {* Explicit term notation *}
text {*
\begin{matharray}{rcll}