doc-src/IsarImplementation/Thy/Logic.thy
changeset 42510 b9c106763325
parent 42401 9bfaf6819291
child 42517 b68e1c27709a
     1.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy	Sat Apr 30 23:27:57 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy	Sun May 01 00:01:59 2011 +0200
     1.3 @@ -197,16 +197,17 @@
     1.4    @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\
     1.5    \end{matharray}
     1.6  
     1.7 -  \begin{rail}
     1.8 -  'class' nameref
     1.9 +  @{rail "
    1.10 +  @@{ML_antiquotation class} nameref
    1.11    ;
    1.12 -  'sort' sort
    1.13 +  @@{ML_antiquotation sort} sort
    1.14    ;
    1.15 -  ('type_name' | 'type_abbrev' | 'nonterminal') nameref
    1.16 +  (@@{ML_antiquotation type_name} |
    1.17 +   @@{ML_antiquotation type_abbrev} |
    1.18 +   @@{ML_antiquotation nonterminal}) nameref
    1.19    ;
    1.20 -  'typ' type
    1.21 -  ;
    1.22 -  \end{rail}
    1.23 +  @@{ML_antiquotation typ} type
    1.24 +  "}
    1.25  
    1.26    \begin{description}
    1.27  
    1.28 @@ -436,16 +437,16 @@
    1.29    @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\
    1.30    \end{matharray}
    1.31  
    1.32 -  \begin{rail}
    1.33 -  ('const_name' | 'const_abbrev') nameref
    1.34 -  ;
    1.35 -  'const' ('(' (type + ',') ')')?
    1.36 +  @{rail "
    1.37 +  (@@{ML_antiquotation const_name} |
    1.38 +   @@{ML_antiquotation const_abbrev}) nameref
    1.39    ;
    1.40 -  'term' term
    1.41 +  @@{ML_antiquotation const} ('(' (type + ',') ')')?
    1.42    ;
    1.43 -  'prop' prop
    1.44 +  @@{ML_antiquotation term} term
    1.45    ;
    1.46 -  \end{rail}
    1.47 +  @@{ML_antiquotation prop} prop
    1.48 +  "}
    1.49  
    1.50    \begin{description}
    1.51  
    1.52 @@ -733,19 +734,20 @@
    1.53    @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\
    1.54    \end{matharray}
    1.55  
    1.56 -  \begin{rail}
    1.57 -  'ctyp' typ
    1.58 +  @{rail "
    1.59 +  @@{ML_antiquotation ctyp} typ
    1.60    ;
    1.61 -  'cterm' term
    1.62 +  @@{ML_antiquotation cterm} term
    1.63    ;
    1.64 -  'cprop' prop
    1.65 +  @@{ML_antiquotation cprop} prop
    1.66    ;
    1.67 -  'thm' thmref
    1.68 +  @@{ML_antiquotation thm} thmref
    1.69 +  ;
    1.70 +  @@{ML_antiquotation thms} thmrefs
    1.71    ;
    1.72 -  'thms' thmrefs
    1.73 -  ;
    1.74 -  'lemma' ('(open)')? ((prop +) + 'and') \\ 'by' method method?
    1.75 -  \end{rail}
    1.76 +  @@{ML_antiquotation lemma} ('(' @@{keyword \"open\"} ')')? ((prop +) + @@{keyword \"and\"}) \\
    1.77 +    @@{keyword \"by\"} method method?
    1.78 +  "}
    1.79  
    1.80    \begin{description}
    1.81