doc-src/IsarRef/Thy/ZF_Specific.thy
changeset 42705 528a2ba8fa74
parent 42704 3f19e324ff59
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 05 23:23:02 2011 +0200
@@ -123,7 +123,7 @@
   \end{matharray}
 
   @{rail "
-    (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goalspec}? @{syntax name}
+    (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
     ;
     @@{method (ZF) ind_cases} (@{syntax prop} +)
     ;