# HG changeset patch
# User wenzelm
# Date 1350478684 -7200
# Node ID 09956f7a00af3f75c3d0245eb584ec3f3913c15b
# Parent  a6563caedf7a28e752ed740ce938795f418706fa
proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;

diff -r a6563caedf7a -r 09956f7a00af 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