doc-src/IsarRef/Thy/Spec.thy
changeset 42625 79e1e99e0a2a
parent 42617 77d239840285
child 42626 6ac8c55c657e
--- a/doc-src/IsarRef/Thy/Spec.thy	Mon May 02 19:55:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Mon May 02 20:14:19 2011 +0200
@@ -171,7 +171,7 @@
   available, and result names need not be given.
 
   @{rail "
-    @@{command axiomatization} @{syntax target}? @{syntax \"fixes\"}? (@'where' specs)?
+    @@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)?
     ;
     @@{command definition} @{syntax target}? (decl @'where')?
       @{syntax thmdecl}? @{syntax prop}