equal
deleted
inserted
replaced
96 |
96 |
97 text %mlref {* |
97 text %mlref {* |
98 \begin{mldecls} |
98 \begin{mldecls} |
99 @{index_ML_type local_theory: Proof.context} \\ |
99 @{index_ML_type local_theory: Proof.context} \\ |
100 @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex] |
100 @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex] |
101 @{index_ML Local_Theory.define: "string -> |
101 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
102 (binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
102 local_theory -> (term * (string * thm)) * local_theory"} \\ |
103 (term * (string * thm)) * local_theory"} \\ |
|
104 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
103 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
105 local_theory -> (string * thm list) * local_theory"} \\ |
104 local_theory -> (string * thm list) * local_theory"} \\ |
106 \end{mldecls} |
105 \end{mldecls} |
107 |
106 |
108 \begin{description} |
107 \begin{description} |
121 @{command locale} or @{command class} context (a fully-qualified |
120 @{command locale} or @{command class} context (a fully-qualified |
122 internal name is expected here). This is useful for experimentation |
121 internal name is expected here). This is useful for experimentation |
123 --- normally the Isar toplevel already takes care to initialize the |
122 --- normally the Isar toplevel already takes care to initialize the |
124 local theory context. |
123 local theory context. |
125 |
124 |
126 \item @{ML Local_Theory.define}~@{text "kind ((b, mx), (a, rhs)) |
125 \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) |
127 lthy"} defines a local entity according to the specification that is |
126 lthy"} defines a local entity according to the specification that is |
128 given relatively to the current @{text "lthy"} context. In |
127 given relatively to the current @{text "lthy"} context. In |
129 particular the term of the RHS may refer to earlier local entities |
128 particular the term of the RHS may refer to earlier local entities |
130 from the auxiliary context, or hypothetical parameters from the |
129 from the auxiliary context, or hypothetical parameters from the |
131 target context. The result is the newly defined term (which is |
130 target context. The result is the newly defined term (which is |
141 context (think of @{command locale} and @{command interpretation}, |
140 context (think of @{command locale} and @{command interpretation}, |
142 for example). This means that attributes should be usually plain |
141 for example). This means that attributes should be usually plain |
143 declarations such as @{attribute simp}, while non-trivial rules like |
142 declarations such as @{attribute simp}, while non-trivial rules like |
144 @{attribute simplified} are better avoided. |
143 @{attribute simplified} are better avoided. |
145 |
144 |
146 The @{text kind} determines the theorem kind tag of the resulting |
|
147 fact. Typical examples are @{ML Thm.definitionK} or @{ML |
|
148 Thm.theoremK}. |
|
149 |
|
150 \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is |
145 \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is |
151 analogous to @{ML Local_Theory.define}, but defines facts instead of |
146 analogous to @{ML Local_Theory.define}, but defines facts instead of |
152 terms. There is also a slightly more general variant @{ML |
147 terms. There is also a slightly more general variant @{ML |
153 Local_Theory.notes} that defines several facts (with attribute |
148 Local_Theory.notes} that defines several facts (with attribute |
154 expressions) simultaneously. |
149 expressions) simultaneously. |