--- 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}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon May 02 19:55:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon May 02 20:14:19 2011 +0200
@@ -224,10 +224,6 @@
\rail@term{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
\rail@endbar
\rail@bar