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: "string -> theory -> local_theory"} \\[1ex] |
94 @{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex] |
95 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
95 @{index_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 @{index_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} |
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 |
103 of the same: a \<^ML_type>\<open>local_theory\<close> holds target information as special |
103 of the same: a \<^ML_type>\<open>local_theory\<close> holds target information as special |
104 context data. Subtyping means that any value \<open>lthy:\<close>~\<^ML_type>\<open>local_theory\<close> |
104 context data. Subtyping means that any value \<open>lthy:\<close>~\<^ML_type>\<open>local_theory\<close> |
105 can be also used with operations on expecting a regular \<open>ctxt:\<close>~\<^ML_type>\<open>Proof.context\<close>. |
105 can be also used with operations on expecting a regular \<open>ctxt:\<close>~\<^ML_type>\<open>Proof.context\<close>. |
106 |
106 |
107 \<^descr> \<^ML>\<open>Named_Target.init\<close>~\<open>before_exit name thy\<close> initializes a local theory |
107 \<^descr> \<^ML>\<open>Named_Target.init\<close>~\<open>includes name thy\<close> initializes a local theory |
108 derived from the given background theory. An empty name refers to a \<^emph>\<open>global |
108 derived from the given background theory. An empty name refers to a \<^emph>\<open>global |
109 theory\<close> context, and a non-empty name refers to a @{command locale} or |
109 theory\<close> context, and a non-empty name refers to a @{command locale} or |
110 @{command class} context (a fully-qualified internal name is expected here). |
110 @{command class} context (a fully-qualified internal name is expected here). |
111 This is useful for experimentation --- normally the Isar toplevel already |
111 This is useful for experimentation --- normally the Isar toplevel already |
112 takes care to initialize the local theory context. |
112 takes care to initialize the local theory context. |