--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Fri Mar 23 09:40:43 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Fri Mar 23 09:40:45 2007 +0100
@@ -253,7 +253,7 @@
separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, 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