103 local_theory -> (string * thm list) * local_theory"} \\ |
103 local_theory -> (string * thm list) * local_theory"} \\ |
104 \end{mldecls} |
104 \end{mldecls} |
105 |
105 |
106 \begin{description} |
106 \begin{description} |
107 |
107 |
108 \item Type @{ML_type local_theory} represents local theories. |
108 \<^descr> Type @{ML_type local_theory} represents local theories. |
109 Although this is merely an alias for @{ML_type Proof.context}, it is |
109 Although this is merely an alias for @{ML_type Proof.context}, it is |
110 semantically a subtype of the same: a @{ML_type local_theory} holds |
110 semantically a subtype of the same: a @{ML_type local_theory} holds |
111 target information as special context data. Subtyping means that |
111 target information as special context data. Subtyping means that |
112 any value @{text "lthy:"}~@{ML_type local_theory} can be also used |
112 any value @{text "lthy:"}~@{ML_type local_theory} can be also used |
113 with operations on expecting a regular @{text "ctxt:"}~@{ML_type |
113 with operations on expecting a regular @{text "ctxt:"}~@{ML_type |
114 Proof.context}. |
114 Proof.context}. |
115 |
115 |
116 \item @{ML Named_Target.init}~@{text "before_exit name thy"} |
116 \<^descr> @{ML Named_Target.init}~@{text "before_exit name thy"} |
117 initializes a local theory derived from the given background theory. |
117 initializes a local theory derived from the given background theory. |
118 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 |
119 non-empty name refers to a @{command locale} or @{command class} |
119 non-empty name refers to a @{command locale} or @{command class} |
120 context (a fully-qualified internal name is expected here). This is |
120 context (a fully-qualified internal name is expected here). This is |
121 useful for experimentation --- normally the Isar toplevel already |
121 useful for experimentation --- normally the Isar toplevel already |
122 takes care to initialize the local theory context. |
122 takes care to initialize the local theory context. |
123 |
123 |
124 \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) |
124 \<^descr> @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) |
125 lthy"} defines a local entity according to the specification that is |
125 lthy"} defines a local entity according to the specification that is |
126 given relatively to the current @{text "lthy"} context. In |
126 given relatively to the current @{text "lthy"} context. In |
127 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 |
128 from the auxiliary context, or hypothetical parameters from the |
128 from the auxiliary context, or hypothetical parameters from the |
129 target context. The result is the newly defined term (which is |
129 target context. The result is the newly defined term (which is |
139 context (think of @{command locale} and @{command interpretation}, |
139 context (think of @{command locale} and @{command interpretation}, |
140 for example). This means that attributes should be usually plain |
140 for example). This means that attributes should be usually plain |
141 declarations such as @{attribute simp}, while non-trivial rules like |
141 declarations such as @{attribute simp}, while non-trivial rules like |
142 @{attribute simplified} are better avoided. |
142 @{attribute simplified} are better avoided. |
143 |
143 |
144 \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is |
144 \<^descr> @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is |
145 analogous to @{ML Local_Theory.define}, but defines facts instead of |
145 analogous to @{ML Local_Theory.define}, but defines facts instead of |
146 terms. There is also a slightly more general variant @{ML |
146 terms. There is also a slightly more general variant @{ML |
147 Local_Theory.notes} that defines several facts (with attribute |
147 Local_Theory.notes} that defines several facts (with attribute |
148 expressions) simultaneously. |
148 expressions) simultaneously. |
149 |
149 |