95 *} |
95 *} |
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 Named_Target.init: "string option -> theory -> local_theory"} \\[1ex] |
100 @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex] |
101 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
101 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
102 local_theory -> (term * (string * thm)) * local_theory"} \\ |
102 local_theory -> (term * (string * thm)) * local_theory"} \\ |
103 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
103 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
104 local_theory -> (string * thm list) * local_theory"} \\ |
104 local_theory -> (string * thm list) * local_theory"} \\ |
105 \end{mldecls} |
105 \end{mldecls} |
112 target information as special context data. Subtyping means that |
112 target information as special context data. Subtyping means that |
113 any value @{text "lthy:"}~@{ML_type local_theory} can be also used |
113 any value @{text "lthy:"}~@{ML_type local_theory} can be also used |
114 with operations on expecting a regular @{text "ctxt:"}~@{ML_type |
114 with operations on expecting a regular @{text "ctxt:"}~@{ML_type |
115 Proof.context}. |
115 Proof.context}. |
116 |
116 |
117 \item @{ML Named_Target.init}~@{text "NONE thy"} initializes a |
117 \item @{ML Named_Target.init}~@{text "name thy"} initializes a local |
118 trivial local theory from the given background theory. |
118 theory derived from the given background theory. An empty name |
119 Alternatively, @{text "SOME name"} may be given to initialize a |
119 refers to a \emph{global theory} context, and a non-empty name |
120 @{command locale} or @{command class} context (a fully-qualified |
120 refers to a @{command locale} or @{command class} context (a |
121 internal name is expected here). This is useful for experimentation |
121 fully-qualified internal name is expected here). This is useful for |
122 --- normally the Isar toplevel already takes care to initialize the |
122 experimentation --- normally the Isar toplevel already takes care to |
123 local theory context. |
123 initialize the local theory context. |
124 |
124 |
125 \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) |
125 \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) |
126 lthy"} defines a local entity according to the specification that is |
126 lthy"} defines a local entity according to the specification that is |
127 given relatively to the current @{text "lthy"} context. In |
127 given relatively to the current @{text "lthy"} context. In |
128 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 |