# HG changeset patch
# User kleing
# Date 1316560621 -36000
# Node ID 07a0638c351ad28482d82263011a9c22a7f21eaf
# Parent  a5d43ffc95eb13d62fdaebb9f204fb1c1c07cf04
fixed two typos in IMP (by Jean Pichon)

diff -r a5d43ffc95eb -r 07a0638c351a src/HOL/IMP/AbsInt1.thy
--- a/src/HOL/IMP/AbsInt1.thy	Wed Sep 21 00:12:36 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy	Wed Sep 21 09:17:01 2011 +1000
@@ -122,7 +122,7 @@
 
 text{* The test for @{const Bot} in the @{const V}-case is important: @{const
 Bot} indicates that a variable has no possible values, i.e.\ that the current
-program point is unreachable. But then the abstract state should collaps to
+program point is unreachable. But then the abstract state should collapse to
 @{const bot}. Put differently, we maintain the invariant that in an abstract
 state all variables are mapped to non-@{const Bot} values. Otherwise the
 (pointwise) join of two abstract states, one of which contains @{const Bot}
diff -r a5d43ffc95eb -r 07a0638c351a src/HOL/IMP/AbsInt2.thy
--- a/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 00:12:36 2011 +0200
+++ b/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 09:17:01 2011 +1000
@@ -6,7 +6,7 @@
 
 subsection "Widening and Narrowing"
 
-text{* The assumptions about winden and narrow are merely sanity checks. They
+text{* The assumptions about widen and narrow are merely sanity checks. They
 are only needed in case we want to prove termination of the fixedpoint
 iteration, which we do not --- we limit the number of iterations as before. *}