--- a/src/HOL/IMP/Abs_Int3.thy Wed Oct 17 14:39:00 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Wed Oct 17 14:58:04 2012 +0200
@@ -704,5 +704,6 @@
which is again not a pfp: not f 2 = 3 <= 2
Another widening step yields 2 widen f 2 = 2 widen 3 = 3
*)
+oops
end