diff -r da8f6f4a74be -r accab7594b8e doc-src/IsarRef/Thy/Inner_Syntax.thy
--- 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}