# HG changeset patch
# User nipkow
# Date 1316903569 -7200
# Node ID 9bcbdf9876015aef73cb0ed132804381018ff202
# Parent  e30442a2b3b2da832b3ddd0397bdab9baeba463a
fixed typo

diff -r e30442a2b3b2 -r 9bcbdf987601 src/HOL/IMP/AbsInt2.thy
--- a/src/HOL/IMP/AbsInt2.thy	Sat Sep 24 17:18:39 2011 +0200
+++ b/src/HOL/IMP/AbsInt2.thy	Sun Sep 25 00:32:49 2011 +0200
@@ -36,7 +36,7 @@
 being iterated to be monotone. Unfortunately, abstract interpretation with
 widening is not monotone. Hence the (recursive) abstract interpretation of a
 loop body that again contains a loop may result in a non-monotone
-function. Therefore our narrowing interation needs to check at every step
+function. Therefore our narrowing iteration needs to check at every step
 that a post-fixed point is maintained, and we cannot prove that the precision
 increases. *}