# HG changeset patch # User wenzelm # Date 1234993492 -3600 # Node ID da411bda1d41e64bbdb4333c99ab9159e9c965fe # Parent 9930a0d8dd3256385cbb9f4676dcb69e4460dc00 tuned; diff -r 9930a0d8dd32 -r da411bda1d41 doc-src/IsarImplementation/Thy/Local_Theory.thy --- a/doc-src/IsarImplementation/Thy/Local_Theory.thy Wed Feb 18 22:37:57 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy Wed Feb 18 22:44:52 2009 +0100 @@ -119,16 +119,16 @@ \item @{ML TheoryTarget.init}~@{text "NONE thy"} initializes a trivial local theory from the given background theory. Alternatively, @{text "SOME name"} may be given to initialize a - locale or class context (a fully-qualified internal name is expected - here). This is useful for experimentation --- normally the Isar - toplevel already takes care to initialize particular local theory - contexts according to user specifications. + @{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 LocalTheory.define}~@{text "kind ((b, mx), (a, rhs)) lthy"} defines a local entity according to the specification that is given relatively to the current @{text "lthy"} context. In particular the term of the RHS may refer to earlier local entities - from the auxiliary context or hypothetical parameters from the + from the auxiliary context, or hypothetical parameters from the target context. The result is the newly defined term (which is always a fixed variable with exactly the same name as specified for the LHS), together with an equational theorem that states the @@ -137,16 +137,16 @@ Unless an explicit name binding is given for the RHS, the resulting fact will be called @{text "b_def"}. Any given attributes are applied to that same fact --- immediately in the auxiliary context - \emph{and} in any transformations stemming from target-specific + \emph{and} in any transformed versions stemming from target-specific policies or any later interpretations of results from the target context (think of @{command locale} and @{command interpretation}, for example). This means that attributes should be usually plain declarations such as @{attribute simp}, while non-trivial rules like @{attribute simplified} are better avoided. - The @{text kind} determines the theorem kind of the resulting fact. - Typical examples are @{ML Thm.definitionK}, @{ML Thm.theoremK}, or - @{ML Thm.internalK}. + The @{text kind} determines the theorem kind tag of the resulting + fact. Typical examples are @{ML Thm.definitionK}, @{ML + Thm.theoremK}, or @{ML Thm.internalK}. \item @{ML LocalTheory.note}~@{text "kind (a, ths) lthy"} is analogous to @{ML LocalTheory.define}, but defines facts instead of