# HG changeset patch
# User wenzelm
# Date 1173723828 -3600
# Node ID 96e650157b1e21ed1b3db07f5893b6298bdf5bbb
# Parent  b3526cd2a3368d8e3eefdf04fd10f4e09ee4c96f
tuned;

diff -r b3526cd2a336 -r 96e650157b1e doc-src/IsarImplementation/Thy/prelim.thy
--- 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