--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy Fri Jan 21 10:35:53 2011 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy Fri Jan 21 17:33:55 2011 +0100
@@ -96,7 +96,8 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type local_theory: Proof.context} \\
- @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
+ @{index_ML Named_Target.init: "(local_theory -> local_theory) ->
+ string -> theory -> local_theory"} \\[1ex]
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory"} \\
@{index_ML Local_Theory.note: "Attrib.binding * thm list ->
@@ -113,13 +114,15 @@
with operations on expecting a regular @{text "ctxt:"}~@{ML_type
Proof.context}.
- \item @{ML Named_Target.init}~@{text "name thy"} initializes a local
- theory derived from the given background theory. An empty name
- refers to a \emph{global theory} context, and a non-empty name
- refers to a @{command locale} or @{command class} context (a
- fully-qualified internal name is expected here). This is useful for
- experimentation --- normally the Isar toplevel already takes care to
- initialize the local theory context.
+ \item @{ML Named_Target.init}~@{text "before_exit name thy"}
+ initializes a local theory derived from the given background theory.
+ An empty name refers to a \emph{global theory} context, and a
+ non-empty name refers to a @{command locale} or @{command class}
+ context (a fully-qualified internal name is expected here). This is
+ useful for experimentation --- normally the Isar toplevel already
+ takes care to initialize the local theory context. The given @{text
+ "before_exit"} function is invoked before leaving the context; in
+ most situations plain identity @{ML I} is sufficient.
\item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
lthy"} defines a local entity according to the specification that is
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Fri Jan 21 10:35:53 2011 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Fri Jan 21 17:33:55 2011 +0100
@@ -122,7 +122,8 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
- \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex]
+ \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: (local_theory -> local_theory) ->|\isasep\isanewline%
+\verb| string -> theory -> local_theory| \\[1ex]
\indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
\verb| local_theory -> (term * (string * thm)) * local_theory| \\
\indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
@@ -138,13 +139,14 @@
any value \isa{lthy{\isaliteral{3A}{\isacharcolon}}}~\verb|local_theory| can be also used
with operations on expecting a regular \isa{ctxt{\isaliteral{3A}{\isacharcolon}}}~\verb|Proof.context|.
- \item \verb|Named_Target.init|~\isa{name\ thy} initializes a local
- theory derived from the given background theory. An empty name
- refers to a \emph{global theory} context, and a non-empty name
- refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a
- fully-qualified internal name is expected here). This is useful for
- experimentation --- normally the Isar toplevel already takes care to
- initialize the local theory context.
+ \item \verb|Named_Target.init|~\isa{before{\isaliteral{5F}{\isacharunderscore}}exit\ name\ thy}
+ initializes a local theory derived from the given background theory.
+ An empty name refers to a \emph{global theory} context, and a
+ non-empty name refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}
+ context (a fully-qualified internal name is expected here). This is
+ useful for experimentation --- normally the Isar toplevel already
+ takes care to initialize the local theory context. The given \isa{before{\isaliteral{5F}{\isacharunderscore}}exit} function is invoked before leaving the context; in
+ most situations plain identity \verb|I| is sufficient.
\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
given relatively to the current \isa{lthy} context. In