120 \isatagmlref |
120 \isatagmlref |
121 % |
121 % |
122 \begin{isamarkuptext}% |
122 \begin{isamarkuptext}% |
123 \begin{mldecls} |
123 \begin{mldecls} |
124 \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\ |
124 \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\ |
125 \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex] |
125 \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: (local_theory -> local_theory) ->|\isasep\isanewline% |
|
126 \verb| string -> theory -> local_theory| \\[1ex] |
126 \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% |
127 \verb| local_theory -> (term * (string * thm)) * local_theory| \\ |
128 \verb| local_theory -> (term * (string * thm)) * local_theory| \\ |
128 \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% |
129 \verb| local_theory -> (string * thm list) * local_theory| \\ |
130 \verb| local_theory -> (string * thm list) * local_theory| \\ |
130 \end{mldecls} |
131 \end{mldecls} |
136 semantically a subtype of the same: a \verb|local_theory| holds |
137 semantically a subtype of the same: a \verb|local_theory| holds |
137 target information as special context data. Subtyping means that |
138 target information as special context data. Subtyping means that |
138 any value \isa{lthy{\isaliteral{3A}{\isacharcolon}}}~\verb|local_theory| can be also used |
139 any value \isa{lthy{\isaliteral{3A}{\isacharcolon}}}~\verb|local_theory| can be also used |
139 with operations on expecting a regular \isa{ctxt{\isaliteral{3A}{\isacharcolon}}}~\verb|Proof.context|. |
140 with operations on expecting a regular \isa{ctxt{\isaliteral{3A}{\isacharcolon}}}~\verb|Proof.context|. |
140 |
141 |
141 \item \verb|Named_Target.init|~\isa{name\ thy} initializes a local |
142 \item \verb|Named_Target.init|~\isa{before{\isaliteral{5F}{\isacharunderscore}}exit\ name\ thy} |
142 theory derived from the given background theory. An empty name |
143 initializes a local theory derived from the given background theory. |
143 refers to a \emph{global theory} context, and a non-empty name |
144 An empty name refers to a \emph{global theory} context, and a |
144 refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a |
145 non-empty name refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} |
145 fully-qualified internal name is expected here). This is useful for |
146 context (a fully-qualified internal name is expected here). This is |
146 experimentation --- normally the Isar toplevel already takes care to |
147 useful for experimentation --- normally the Isar toplevel already |
147 initialize the local theory context. |
148 takes care to initialize the local theory context. The given \isa{before{\isaliteral{5F}{\isacharunderscore}}exit} function is invoked before leaving the context; in |
|
149 most situations plain identity \verb|I| is sufficient. |
148 |
150 |
149 \item \verb|Local_Theory.define|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}b{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ lthy} defines a local entity according to the specification that is |
151 \item \verb|Local_Theory.define|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}b{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ lthy} defines a local entity according to the specification that is |
150 given relatively to the current \isa{lthy} context. In |
152 given relatively to the current \isa{lthy} context. In |
151 particular the term of the RHS may refer to earlier local entities |
153 particular the term of the RHS may refer to earlier local entities |
152 from the auxiliary context, or hypothetical parameters from the |
154 from the auxiliary context, or hypothetical parameters from the |