# HG changeset patch
# User wenzelm
# Date 1408184156 -7200
# Node ID 189d421ca72d4baba8ff550e52c4f59a09171496
# Parent  6a26aa5fa65e3aa6366910019c1c29babe02ae07
updated syntax for localized commands;

diff -r 6a26aa5fa65e -r 189d421ca72d src/Doc/Isar_Ref/Proof.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}
diff -r 6a26aa5fa65e -r 189d421ca72d src/Doc/Isar_Ref/Spec.thy
--- 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}