# HG changeset patch
# User wenzelm
# Date 1304360059 -7200
# Node ID 79e1e99e0a2a8605b0e77130ca357a29c5690d8a
# Parent  07fc82c444d25b9d95d30ad5a7701e2e31912a78
'axiomatization' is global;

diff -r 07fc82c444d2 -r 79e1e99e0a2a doc-src/IsarRef/Thy/Spec.thy
--- 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}
diff -r 07fc82c444d2 -r 79e1e99e0a2a doc-src/IsarRef/Thy/document/Spec.tex
--- 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