# HG changeset patch # User wenzelm # Date 1234816759 -3600 # Node ID 2b658e50683aabd4fb99cebafd147da1db699462 # Parent 9c6c1b3f3eb6fd15b844afcf7e26e85562ac3e47 minor tuning and typographic fixes; diff -r 9c6c1b3f3eb6 -r 2b658e50683a doc-src/IsarImplementation/Thy/Integration.thy --- a/doc-src/IsarImplementation/Thy/Integration.thy Mon Feb 16 21:23:34 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Integration.thy Mon Feb 16 21:39:19 2009 +0100 @@ -122,7 +122,7 @@ Internally, Isar commands are put together from an empty transition extended by name and source position (and optional source text). It is then left to the individual command parser to turn the given - concrete syntax into a suitable transition transformer that adjoin + concrete syntax into a suitable transition transformer that adjoins actual operations on a theory or proof state etc. *} diff -r 9c6c1b3f3eb6 -r 2b658e50683a doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:23:34 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:39:19 2009 +0100 @@ -191,9 +191,9 @@ text {* The language of terms is that of simply-typed @{text "\"}-calculus with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72} - or \cite{paulson-ml2}), with the types being determined determined - by the corresponding binders. In contrast, free variables and - constants are have an explicit name and type in each occurrence. + or \cite{paulson-ml2}), with the types being determined by the + corresponding binders. In contrast, free variables and constants + are have an explicit name and type in each occurrence. \medskip A \emph{bound variable} is a natural number @{text "b"}, which accounts for the number of intermediate binders between the diff -r 9c6c1b3f3eb6 -r 2b658e50683a doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Mon Feb 16 21:23:34 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Mon Feb 16 21:39:19 2009 +0100 @@ -74,7 +74,7 @@ subsection {* Theory context \label{sec:context-theory} *} text {* - A \emph{theory} is a data container with explicit named and unique + A \emph{theory} is a data container with explicit name and unique identifier. Theories are related by a (nominal) sub-theory relation, which corresponds to the dependency graph of the original construction; each theory is derived from a certain sub-graph of @@ -178,7 +178,7 @@ \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text "thy"} that holds a copy of the same data. The result is not - related to the original; the original is unchanched. + related to the original; the original is unchanged. \item @{ML_type theory_ref} represents a sliding reference to an always valid theory; updates on the original are propagated @@ -213,7 +213,7 @@ identification as for theories. For example, hypotheses used in primitive derivations (cf.\ \secref{sec:thms}) are recorded separately within the sequent @{text "\ \ \"}, just to make double - sure. Results could still leak into an alien proof context do to + sure. Results could still leak into an alien proof context due to programming errors, but Isabelle/Isar includes some extra validity checks in critical positions, notably at the end of a sub-proof. @@ -353,7 +353,7 @@ \medskip \begin{tabular}{ll} - @{text "init: theory \ theory"} \\ + @{text "init: theory \ T"} \\ @{text "get: context \ T"} \\ @{text "put: T \ context \ context"} \\ @{text "map: (T \ T) \ context \ context"} \\ @@ -505,10 +505,9 @@ text {* A \emph{basic name} essentially consists of a single Isabelle identifier. There are conventions to mark separate classes of basic - names, by attaching a suffix of underscores (@{text "_"}): one - underscore means \emph{internal name}, two underscores means - \emph{Skolem name}, three underscores means \emph{internal Skolem - name}. + names, by attaching a suffix of underscores: one underscore means + \emph{internal name}, two underscores means \emph{Skolem name}, + three underscores means \emph{internal Skolem name}. For example, the basic name @{text "foo"} has the internal version @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text @@ -568,7 +567,7 @@ "n"} fresh names derived from @{text "name"}. \item @{ML Name.variants}~@{text "names context"} produces fresh - varians of @{text "names"}; the result is entered into the context. + variants of @{text "names"}; the result is entered into the context. \end{description} *} diff -r 9c6c1b3f3eb6 -r 2b658e50683a doc-src/IsarImplementation/Thy/Proof.thy --- a/doc-src/IsarImplementation/Thy/Proof.thy Mon Feb 16 21:23:34 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Mon Feb 16 21:39:19 2009 +0100 @@ -302,11 +302,11 @@ \begin{description} - \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a - particular sub-goal, producing an extended context and a reduced - goal, which needs to be solved by the given tactic. All schematic - parameters of the goal are imported into the context as fixed ones, - which may not be instantiated in the sub-proof. + \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure + of the specified sub-goal, producing an extended context and a + reduced goal, which needs to be solved by the given tactic. All + schematic parameters of the goal are imported into the context as + fixed ones, which may not be instantiated in the sub-proof. \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text "C"} in the context augmented by fixed variables @{text "xs"} and diff -r 9c6c1b3f3eb6 -r 2b658e50683a doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Mon Feb 16 21:23:34 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Mon Feb 16 21:39:19 2009 +0100 @@ -27,15 +27,16 @@ instantiated during the course of reasoning.}. For @{text "n = 0"} a goal is called ``solved''. - The structure of each subgoal @{text "A\<^sub>i"} is that of a general - Hereditary Harrop Formula @{text "\x\<^sub>1 \ \x\<^sub>k. H\<^sub>1 \ \ \ H\<^sub>m \ B"} in - normal form. Here @{text "x\<^sub>1, \, x\<^sub>k"} are goal parameters, i.e.\ - arbitrary-but-fixed entities of certain types, and @{text "H\<^sub>1, \, - H\<^sub>m"} are goal hypotheses, i.e.\ facts that may be assumed locally. - Together, this forms the goal context of the conclusion @{text B} to - be established. The goal hypotheses may be again arbitrary - Hereditary Harrop Formulas, although the level of nesting rarely - exceeds 1--2 in practice. + The structure of each subgoal @{text "A\<^sub>i"} is that of a + general Hereditary Harrop Formula @{text "\x\<^sub>1 \ + \x\<^sub>k. H\<^sub>1 \ \ \ H\<^sub>m \ B"}. Here @{text + "x\<^sub>1, \, x\<^sub>k"} are goal parameters, i.e.\ + arbitrary-but-fixed entities of certain types, and @{text + "H\<^sub>1, \, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may + be assumed locally. Together, this forms the goal context of the + conclusion @{text B} to be established. The goal hypotheses may be + again arbitrary Hereditary Harrop Formulas, although the level of + nesting rarely exceeds 1--2 in practice. The main conclusion @{text C} is internally marked as a protected proposition, which is represented explicitly by the notation @{text