--- a/doc-src/IsarImplementation/Thy/prelim.thy Mon Mar 12 16:25:39 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Mon Mar 12 19:23:48 2007 +0100
@@ -223,7 +223,7 @@
separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to make double
sure. Results could still leak into an alien proof context do to
programming errors, but Isabelle/Isar includes some extra validity
- checks in critical positions, notably at the end of sub-proof.
+ checks in critical positions, notably at the end of a sub-proof.
Proof contexts may be manipulated arbitrarily, although the common
discipline is to follow block structure as a mental model: a given