1.1 --- a/doc-src/IsarImplementation/Thy/Local_Theory.thy Sat Nov 21 16:07:58 2009 +0100
1.2 +++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy Sat Nov 21 17:01:44 2009 +0100
1.3 @@ -98,9 +98,8 @@
1.4 \begin{mldecls}
1.5 @{index_ML_type local_theory: Proof.context} \\
1.6 @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex]
1.7 - @{index_ML Local_Theory.define: "string ->
1.8 - (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
1.9 - (term * (string * thm)) * local_theory"} \\
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 local_theory -> (string * thm list) * local_theory"} \\
1.14 \end{mldecls}
1.15 @@ -123,7 +122,7 @@
1.16 --- normally the Isar toplevel already takes care to initialize the
1.17 local theory context.
1.18
1.19 - \item @{ML Local_Theory.define}~@{text "kind ((b, mx), (a, rhs))
1.20 + \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
1.21 lthy"} defines a local entity according to the specification that is
1.22 given relatively to the current @{text "lthy"} context. In
1.23 particular the term of the RHS may refer to earlier local entities
1.24 @@ -143,10 +142,6 @@
1.25 declarations such as @{attribute simp}, while non-trivial rules like
1.26 @{attribute simplified} are better avoided.
1.27
1.28 - The @{text kind} determines the theorem kind tag of the resulting
1.29 - fact. Typical examples are @{ML Thm.definitionK} or @{ML
1.30 - Thm.theoremK}.
1.31 -
1.32 \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is
1.33 analogous to @{ML Local_Theory.define}, but defines facts instead of
1.34 terms. There is also a slightly more general variant @{ML
2.1 --- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Sat Nov 21 16:07:58 2009 +0100
2.2 +++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Sat Nov 21 17:01:44 2009 +0100
2.3 @@ -124,9 +124,8 @@
2.4 \begin{mldecls}
2.5 \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
2.6 \indexdef{}{ML}{Theory\_Target.init}\verb|Theory_Target.init: string option -> theory -> local_theory| \\[1ex]
2.7 - \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: string ->|\isasep\isanewline%
2.8 -\verb| (binding * mixfix) * (Attrib.binding * term) -> local_theory ->|\isasep\isanewline%
2.9 -\verb| (term * (string * thm)) * local_theory| \\
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 \verb| local_theory -> (string * thm list) * local_theory| \\
2.14 \end{mldecls}
2.15 @@ -148,7 +147,7 @@
2.16 --- normally the Isar toplevel already takes care to initialize the
2.17 local theory context.
2.18
2.19 - \item \verb|Local_Theory.define|~\isa{kind\ {\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is
2.20 + \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
2.21 given relatively to the current \isa{lthy} context. In
2.22 particular the term of the RHS may refer to earlier local entities
2.23 from the auxiliary context, or hypothetical parameters from the
2.24 @@ -167,9 +166,6 @@
2.25 declarations such as \hyperlink{attribute.simp}{\mbox{\isa{simp}}}, while non-trivial rules like
2.26 \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}} are better avoided.
2.27
2.28 - The \isa{kind} determines the theorem kind tag of the resulting
2.29 - fact. Typical examples are \verb|Thm.definitionK| or \verb|Thm.theoremK|.
2.30 -
2.31 \item \verb|Local_Theory.note|~\isa{{\isacharparenleft}a{\isacharcomma}\ ths{\isacharparenright}\ lthy} is
2.32 analogous to \verb|Local_Theory.define|, but defines facts instead of
2.33 terms. There is also a slightly more general variant \verb|Local_Theory.notes| that defines several facts (with attribute