Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Mon, 12 Mar 2007 19:23:48 +0100
changeset 22438 96e650157b1e
parent 22437 b3526cd2a336
child 22439 b709739c69e6
tuned;
doc-src/IsarImplementation/Thy/prelim.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle