121 \isatagmlref |
121 \isatagmlref |
122 % |
122 % |
123 \begin{isamarkuptext}% |
123 \begin{isamarkuptext}% |
124 \begin{mldecls} |
124 \begin{mldecls} |
125 \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\ |
125 \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\ |
126 \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string option -> theory -> local_theory| \\[1ex] |
126 \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex] |
127 \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline% |
127 \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline% |
128 \verb| local_theory -> (term * (string * thm)) * local_theory| \\ |
128 \verb| local_theory -> (term * (string * thm)) * local_theory| \\ |
129 \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline% |
129 \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline% |
130 \verb| local_theory -> (string * thm list) * local_theory| \\ |
130 \verb| local_theory -> (string * thm list) * local_theory| \\ |
131 \end{mldecls} |
131 \end{mldecls} |
137 semantically a subtype of the same: a \verb|local_theory| holds |
137 semantically a subtype of the same: a \verb|local_theory| holds |
138 target information as special context data. Subtyping means that |
138 target information as special context data. Subtyping means that |
139 any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used |
139 any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used |
140 with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|. |
140 with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|. |
141 |
141 |
142 \item \verb|Named_Target.init|~\isa{NONE\ thy} initializes a |
142 \item \verb|Named_Target.init|~\isa{name\ thy} initializes a local |
143 trivial local theory from the given background theory. |
143 theory derived from the given background theory. An empty name |
144 Alternatively, \isa{SOME\ name} may be given to initialize a |
144 refers to a \emph{global theory} context, and a non-empty name |
145 \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified |
145 refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a |
146 internal name is expected here). This is useful for experimentation |
146 fully-qualified internal name is expected here). This is useful for |
147 --- normally the Isar toplevel already takes care to initialize the |
147 experimentation --- normally the Isar toplevel already takes care to |
148 local theory context. |
148 initialize the local theory context. |
149 |
149 |
150 \item \verb|Local_Theory.define|~\isa{{\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is |
150 \item \verb|Local_Theory.define|~\isa{{\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is |
151 given relatively to the current \isa{lthy} context. In |
151 given relatively to the current \isa{lthy} context. In |
152 particular the term of the RHS may refer to earlier local entities |
152 particular the term of the RHS may refer to earlier local entities |
153 from the auxiliary context, or hypothetical parameters from the |
153 from the auxiliary context, or hypothetical parameters from the |