--- a/src/HOL/IMP/AbsInt1_ivl.thy Wed Sep 21 02:38:53 2011 +0200
+++ b/src/HOL/IMP/AbsInt1_ivl.thy Wed Sep 21 03:24:54 2011 +0200
@@ -150,7 +150,8 @@
fun inv_less_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool \<Rightarrow> ivl * ivl" where
"inv_less_ivl (I l1 h1) (I l2 h2) res =
- (if res
+ ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
+ if res
then (I l1 (min_option True h1 (h2 - Some 1)),
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
--- a/src/HOL/IMP/AbsInt2.thy Wed Sep 21 02:38:53 2011 +0200
+++ b/src/HOL/IMP/AbsInt2.thy Wed Sep 21 03:24:54 2011 +0200
@@ -66,8 +66,7 @@
begin
definition "widen_ivl ivl1 ivl2 =
- ((*if is_empty ivl1 then ivl2 else
- if is_empty ivl2 then ivl1 else*)
+ ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
(if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"