--- 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}
--- 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. *}