src/Doc/Implementation/Logic.thy
changeset 67146 909dcdec2122
parent 65446 ed18feb34c07
child 68540 000a0e062529
     1.1 --- a/src/Doc/Implementation/Logic.thy	Wed Dec 06 14:19:36 2017 +0100
     1.2 +++ b/src/Doc/Implementation/Logic.thy	Wed Dec 06 15:46:35 2017 +0100
     1.3 @@ -171,13 +171,13 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail \<open>
     1.7 -  @@{ML_antiquotation class} name
     1.8 +  @@{ML_antiquotation class} embedded
     1.9    ;
    1.10    @@{ML_antiquotation sort} sort
    1.11    ;
    1.12    (@@{ML_antiquotation type_name} |
    1.13     @@{ML_antiquotation type_abbrev} |
    1.14 -   @@{ML_antiquotation nonterminal}) name
    1.15 +   @@{ML_antiquotation nonterminal}) embedded
    1.16    ;
    1.17    @@{ML_antiquotation typ} type
    1.18    \<close>}
    1.19 @@ -392,7 +392,7 @@
    1.20  
    1.21    @{rail \<open>
    1.22    (@@{ML_antiquotation const_name} |
    1.23 -   @@{ML_antiquotation const_abbrev}) name
    1.24 +   @@{ML_antiquotation const_abbrev}) embedded
    1.25    ;
    1.26    @@{ML_antiquotation const} ('(' (type + ',') ')')?
    1.27    ;