updated syntax for localized commands;
authorwenzelm
Sat, 16 Aug 2014 12:15:56 +0200
changeset 57947 189d421ca72d
parent 57946 6a26aa5fa65e
child 57948 75724d71013c
updated syntax for localized commands;
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sat Aug 16 12:10:36 2014 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat Aug 16 12:15:56 2014 +0200
@@ -919,7 +919,8 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
+    @@{command method_setup} @{syntax target}?
+      @{syntax name} '=' @{syntax text} @{syntax text}?
   \<close>}
 
   \begin{description}
--- a/src/Doc/Isar_Ref/Spec.thy	Sat Aug 16 12:10:36 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Aug 16 12:15:56 2014 +0200
@@ -1045,7 +1045,8 @@
     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
     ;
-    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
+    @@{command attribute_setup} @{syntax target}?
+      @{syntax name} '=' @{syntax text} @{syntax text}?
   \<close>}
 
   \begin{description}