# HG changeset patch
# User haftmann
# Date 1174639245 -3600
# Node ID 22b638460a13051dacad2fa5628918e98b0bc279
# Parent  d53664118418814c4ced72531fa5b36b266368de
fixed typo

diff -r d53664118418 -r 22b638460a13 doc-src/IsarImplementation/Thy/document/prelim.tex
--- 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