94 for details). *} |
94 for details). *} |
95 |
95 |
96 text %mlref {* |
96 text %mlref {* |
97 \begin{mldecls} |
97 \begin{mldecls} |
98 @{index_ML_type local_theory: Proof.context} \\ |
98 @{index_ML_type local_theory: Proof.context} \\ |
99 @{index_ML Named_Target.init: "(local_theory -> local_theory) -> |
99 @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex] |
100 string -> theory -> local_theory"} \\[1ex] |
|
101 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
100 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
102 local_theory -> (term * (string * thm)) * local_theory"} \\ |
101 local_theory -> (term * (string * thm)) * local_theory"} \\ |
103 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
102 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
104 local_theory -> (string * thm list) * local_theory"} \\ |
103 local_theory -> (string * thm list) * local_theory"} \\ |
105 \end{mldecls} |
104 \end{mldecls} |
118 initializes a local theory derived from the given background theory. |
117 initializes a local theory derived from the given background theory. |
119 An empty name refers to a \emph{global theory} context, and a |
118 An empty name refers to a \emph{global theory} context, and a |
120 non-empty name refers to a @{command locale} or @{command class} |
119 non-empty name refers to a @{command locale} or @{command class} |
121 context (a fully-qualified internal name is expected here). This is |
120 context (a fully-qualified internal name is expected here). This is |
122 useful for experimentation --- normally the Isar toplevel already |
121 useful for experimentation --- normally the Isar toplevel already |
123 takes care to initialize the local theory context. The given @{text |
122 takes care to initialize the local theory context. |
124 "before_exit"} function is invoked before leaving the context; in |
|
125 most situations plain identity @{ML I} is sufficient. |
|
126 |
123 |
127 \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) |
124 \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) |
128 lthy"} defines a local entity according to the specification that is |
125 lthy"} defines a local entity according to the specification that is |
129 given relatively to the current @{text "lthy"} context. In |
126 given relatively to the current @{text "lthy"} context. In |
130 particular the term of the RHS may refer to earlier local entities |
127 particular the term of the RHS may refer to earlier local entities |