# HG changeset patch
# User nipkow
# Date 1316568294 -7200
# Node ID 4e3b999c62fa9f7c18fd26e6bb1d1bed6c608c10
# Parent  020e460b6644959a8eacfcf6ea30d8ad7a4ea9b6
tuned

diff -r 020e460b6644 -r 4e3b999c62fa src/HOL/IMP/AbsInt1_ivl.thy
--- 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)))"
diff -r 020e460b6644 -r 4e3b999c62fa src/HOL/IMP/AbsInt2.thy
--- 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))"