# 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