updated syntax for localized commands;
authorwenzelm
Sat Aug 16 12:15:56 2014 +0200 (2014-08-16)
changeset 57947189d421ca72d
parent 57946 6a26aa5fa65e
child 57948 75724d71013c
updated syntax for localized commands;
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Spec.thy
     1.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sat Aug 16 12:10:36 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sat Aug 16 12:15:56 2014 +0200
     1.3 @@ -919,7 +919,8 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail \<open>
     1.7 -    @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
     1.8 +    @@{command method_setup} @{syntax target}?
     1.9 +      @{syntax name} '=' @{syntax text} @{syntax text}?
    1.10    \<close>}
    1.11  
    1.12    \begin{description}
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Aug 16 12:10:36 2014 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat Aug 16 12:15:56 2014 +0200
     2.3 @@ -1045,7 +1045,8 @@
     2.4      (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
     2.5        @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
     2.6      ;
     2.7 -    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
     2.8 +    @@{command attribute_setup} @{syntax target}?
     2.9 +      @{syntax name} '=' @{syntax text} @{syntax text}?
    2.10    \<close>}
    2.11  
    2.12    \begin{description}