src/Doc/Implementation/Prelim.thy
changeset 67146 909dcdec2122
parent 62969 9f394a16c557
child 69292 06fda16e50fb
     1.1 --- a/src/Doc/Implementation/Prelim.thy	Wed Dec 06 14:19:36 2017 +0100
     1.2 +++ b/src/Doc/Implementation/Prelim.thy	Wed Dec 06 15:46:35 2017 +0100
     1.3 @@ -142,9 +142,9 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail \<open>
     1.7 -  @@{ML_antiquotation theory} name?
     1.8 +  @@{ML_antiquotation theory} embedded?
     1.9    ;
    1.10 -  @@{ML_antiquotation theory_context} name
    1.11 +  @@{ML_antiquotation theory_context} embedded
    1.12    \<close>}
    1.13  
    1.14    \<^descr> \<open>@{theory}\<close> refers to the background theory of the current context --- as
    1.15 @@ -938,7 +938,7 @@
    1.16    \end{matharray}
    1.17  
    1.18    @{rail \<open>
    1.19 -  @@{ML_antiquotation binding} name
    1.20 +  @@{ML_antiquotation binding} embedded
    1.21    \<close>}
    1.22  
    1.23    \<^descr> \<open>@{binding name}\<close> produces a binding with base name \<open>name\<close> and the source