1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:50:57 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:52:09 2008 +0100
     1.3 @@ -12,32 +12,30 @@
     1.4  
     1.5  text {*
     1.6    \begin{matharray}{rcl}
     1.7 -    @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     1.8 -    @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.9 +    @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.10      @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.11      @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.12 -    @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.13 +    @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.14      @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.15      @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.16 +    @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    1.17    \end{matharray}
    1.18  
    1.19    These diagnostic commands assist interactive development by printing
    1.20    internal logical entities in a human-readable fashion.
    1.21  
    1.22    \begin{rail}
    1.23 -    'pr' modes? nat? (',' nat)?
    1.24 -    ;
    1.25 -    'thm' modes? thmrefs
    1.26 +    'typ' modes? type
    1.27      ;
    1.28      'term' modes? term
    1.29      ;
    1.30      'prop' modes? prop
    1.31      ;
    1.32 -    'typ' modes? type
    1.33 +    'thm' modes? thmrefs
    1.34      ;
    1.35 -    'prf' modes? thmrefs?
    1.36 +    ( 'prf' | 'full\_prf' ) modes? thmrefs?
    1.37      ;
    1.38 -    'full\_prf' modes? thmrefs?
    1.39 +    'pr' modes? nat? (',' nat)?
    1.40      ;
    1.41  
    1.42      modes: '(' (name + ) ')'
    1.43 @@ -46,11 +44,14 @@
    1.44  
    1.45    \begin{description}
    1.46  
    1.47 -  \item @{command "pr"}~@{text "goals, prems"} prints the current
    1.48 -  proof state (if present), including the proof context, current facts
    1.49 -  and goals.  The optional limit arguments affect the number of goals
    1.50 -  and premises to be displayed, which is initially 10 for both.
    1.51 -  Omitting limit values leaves the current setting unchanged.
    1.52 +  \item @{command "typ"}~@{text \<tau>} reads and prints types of the
    1.53 +  meta-logic according to the current theory or proof context.
    1.54 +
    1.55 +  \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
    1.56 +  read, type-check and print terms or propositions according to the
    1.57 +  current theory or proof context; the inferred type of @{text t} is
    1.58 +  output as well.  Note that these commands are also useful in
    1.59 +  inspecting the current environment of term abbreviations.
    1.60  
    1.61    \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
    1.62    theorems from the current theory or proof context.  Note that any
    1.63 @@ -59,15 +60,6 @@
    1.64    result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
    1.65    \<dots>, a\<^sub>n"} do not have any permanent effect.
    1.66  
    1.67 -  \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
    1.68 -  read, type-check and print terms or propositions according to the
    1.69 -  current theory or proof context; the inferred type of @{text t} is
    1.70 -  output as well.  Note that these commands are also useful in
    1.71 -  inspecting the current environment of term abbreviations.
    1.72 -
    1.73 -  \item @{command "typ"}~@{text \<tau>} reads and prints types of the
    1.74 -  meta-logic according to the current theory or proof context.
    1.75 -
    1.76    \item @{command "prf"} displays the (compact) proof term of the
    1.77    current proof state (if present), or of the given theorems. Note
    1.78    that this requires proof terms to be switched on for the current
    1.79 @@ -79,6 +71,12 @@
    1.80    compact proof term, which is denoted by ``@{text _}'' placeholders
    1.81    there.
    1.82  
    1.83 +  \item @{command "pr"}~@{text "goals, prems"} prints the current
    1.84 +  proof state (if present), including the proof context, current facts
    1.85 +  and goals.  The optional limit arguments affect the number of goals
    1.86 +  and premises to be displayed, which is initially 10 for both.
    1.87 +  Omitting limit values leaves the current setting unchanged.
    1.88 +
    1.89    \end{description}
    1.90  
    1.91    All of the diagnostic commands above admit a list of @{text modes}
    1.92 @@ -355,7 +353,7 @@
    1.93  *}
    1.94  
    1.95  
    1.96 -section {* Additional term notation *}
    1.97 +section {* Explicit term notation *}
    1.98  
    1.99  text {*
   1.100    \begin{matharray}{rcll}