doc-src/IsarRef/Thy/Proof.thy

--- a/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 23:23:02 2011 +0200
@@ -194,7 +194,7 @@
     ;
     @@{command def} (def + @'and')
     ;
-    def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax termpat}?
+    def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
   "}
 
   \begin{description}
@@ -269,8 +269,8 @@
     @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')
   "}
 
-  The syntax of @{keyword "is"} patterns follows @{syntax termpat} or
-  @{syntax proppat} (see \secref{sec:term-decls}).
+  The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
+  @{syntax prop_pat} (see \secref{sec:term-decls}).
 
   \begin{description}
 
@@ -568,7 +568,7 @@
   "n"}.
 
   @{rail "
-    @{syntax_def goalspec}:
+    @{syntax_def goal_spec}:
       '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'
   "}
 *}