proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
authorwenzelm
Wed, 17 Oct 2012 14:58:04 +0200
changeset 49892 09956f7a00af
parent 49891 a6563caedf7a
child 49893 0d4106850eb2
proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
src/HOL/IMP/Abs_Int3.thy
--- 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