equal
deleted
inserted
replaced
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 @{index_ML_type local_theory: Proof.context} \\ |
94 @{index_ML Named_Target.init: "(local_theory -> local_theory) option -> |
94 @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex] |
95 string -> theory -> local_theory"} \\[1ex] |
|
96 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
95 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
97 local_theory -> (term * (string * thm)) * local_theory"} \\ |
96 local_theory -> (term * (string * thm)) * local_theory"} \\ |
98 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
97 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
99 local_theory -> (string * thm list) * local_theory"} \\ |
98 local_theory -> (string * thm list) * local_theory"} \\ |
100 \end{mldecls} |
99 \end{mldecls} |