--- 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 "\<Gamma> \<turnstile> \<phi>"}, 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 \<rightarrow> theory"} \\
+ @{text "init: theory \<rightarrow> T"} \\
@{text "get: context \<rightarrow> T"} \\
@{text "put: T \<rightarrow> context \<rightarrow> context"} \\
@{text "map: (T \<rightarrow> T) \<rightarrow> context \<rightarrow> 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}
*}