| changeset 45017 | 07a0638c351a |
| parent 45015 | fdac1e9880eb |
| child 45018 | 020e460b6644 |
--- 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. *}