equal
deleted
inserted
replaced
88 "Haftmann-Wenzel:2009"} for details). |
88 "Haftmann-Wenzel:2009"} for details). |
89 \<close> |
89 \<close> |
90 |
90 |
91 text %mlref \<open> |
91 text %mlref \<open> |
92 \begin{mldecls} |
92 \begin{mldecls} |
93 @{index_ML_type local_theory = Proof.context} \\ |
93 @{define_ML_type local_theory = Proof.context} \\ |
94 @{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex] |
94 @{define_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex] |
95 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
95 @{define_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
96 local_theory -> (term * (string * thm)) * local_theory"} \\ |
96 local_theory -> (term * (string * thm)) * local_theory"} \\ |
97 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
97 @{define_ML Local_Theory.note: "Attrib.binding * thm list -> |
98 local_theory -> (string * thm list) * local_theory"} \\ |
98 local_theory -> (string * thm list) * local_theory"} \\ |
99 \end{mldecls} |
99 \end{mldecls} |
100 |
100 |
101 \<^descr> Type \<^ML_type>\<open>local_theory\<close> represents local theories. Although this is |
101 \<^descr> Type \<^ML_type>\<open>local_theory\<close> represents local theories. Although this is |
102 merely an alias for \<^ML_type>\<open>Proof.context\<close>, it is semantically a subtype |
102 merely an alias for \<^ML_type>\<open>Proof.context\<close>, it is semantically a subtype |