updated Named_Target.init;
authorwenzelm
Fri Jan 21 17:33:55 2011 +0100 (2011-01-21)
changeset 4162155b16bd82142
parent 41620 f88eca2e9ebd
child 41622 ad5474a8374b
updated Named_Target.init;
doc-src/IsarImplementation/Thy/Local_Theory.thy
doc-src/IsarImplementation/Thy/document/Local_Theory.tex
     1.1 --- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Fri Jan 21 10:35:53 2011 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Fri Jan 21 17:33:55 2011 +0100
     1.3 @@ -96,7 +96,8 @@
     1.4  text %mlref {*
     1.5    \begin{mldecls}
     1.6    @{index_ML_type local_theory: Proof.context} \\
     1.7 -  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
     1.8 +  @{index_ML Named_Target.init: "(local_theory -> local_theory) ->
     1.9 +    string -> theory -> local_theory"} \\[1ex]
    1.10    @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
    1.11      local_theory -> (term * (string * thm)) * local_theory"} \\
    1.12    @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
    1.13 @@ -113,13 +114,15 @@
    1.14    with operations on expecting a regular @{text "ctxt:"}~@{ML_type
    1.15    Proof.context}.
    1.16  
    1.17 -  \item @{ML Named_Target.init}~@{text "name thy"} initializes a local
    1.18 -  theory derived from the given background theory.  An empty name
    1.19 -  refers to a \emph{global theory} context, and a non-empty name
    1.20 -  refers to a @{command locale} or @{command class} context (a
    1.21 -  fully-qualified internal name is expected here).  This is useful for
    1.22 -  experimentation --- normally the Isar toplevel already takes care to
    1.23 -  initialize the local theory context.
    1.24 +  \item @{ML Named_Target.init}~@{text "before_exit name thy"}
    1.25 +  initializes a local theory derived from the given background theory.
    1.26 +  An empty name refers to a \emph{global theory} context, and a
    1.27 +  non-empty name refers to a @{command locale} or @{command class}
    1.28 +  context (a fully-qualified internal name is expected here).  This is
    1.29 +  useful for experimentation --- normally the Isar toplevel already
    1.30 +  takes care to initialize the local theory context.  The given @{text
    1.31 +  "before_exit"} function is invoked before leaving the context; in
    1.32 +  most situations plain identity @{ML I} is sufficient.
    1.33  
    1.34    \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
    1.35    lthy"} defines a local entity according to the specification that is
     2.1 --- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Fri Jan 21 10:35:53 2011 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Fri Jan 21 17:33:55 2011 +0100
     2.3 @@ -122,7 +122,8 @@
     2.4  \begin{isamarkuptext}%
     2.5  \begin{mldecls}
     2.6    \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
     2.7 -  \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex]
     2.8 +  \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: (local_theory -> local_theory) ->|\isasep\isanewline%
     2.9 +\verb|    string -> theory -> local_theory| \\[1ex]
    2.10    \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
    2.11  \verb|    local_theory -> (term * (string * thm)) * local_theory| \\
    2.12    \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
    2.13 @@ -138,13 +139,14 @@
    2.14    any value \isa{lthy{\isaliteral{3A}{\isacharcolon}}}~\verb|local_theory| can be also used
    2.15    with operations on expecting a regular \isa{ctxt{\isaliteral{3A}{\isacharcolon}}}~\verb|Proof.context|.
    2.16  
    2.17 -  \item \verb|Named_Target.init|~\isa{name\ thy} initializes a local
    2.18 -  theory derived from the given background theory.  An empty name
    2.19 -  refers to a \emph{global theory} context, and a non-empty name
    2.20 -  refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a
    2.21 -  fully-qualified internal name is expected here).  This is useful for
    2.22 -  experimentation --- normally the Isar toplevel already takes care to
    2.23 -  initialize the local theory context.
    2.24 +  \item \verb|Named_Target.init|~\isa{before{\isaliteral{5F}{\isacharunderscore}}exit\ name\ thy}
    2.25 +  initializes a local theory derived from the given background theory.
    2.26 +  An empty name refers to a \emph{global theory} context, and a
    2.27 +  non-empty name refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}
    2.28 +  context (a fully-qualified internal name is expected here).  This is
    2.29 +  useful for experimentation --- normally the Isar toplevel already
    2.30 +  takes care to initialize the local theory context.  The given \isa{before{\isaliteral{5F}{\isacharunderscore}}exit} function is invoked before leaving the context; in
    2.31 +  most situations plain identity \verb|I| is sufficient.
    2.32  
    2.33    \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
    2.34    given relatively to the current \isa{lthy} context.  In