diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -23,10 +23,12 @@
 instantiation const :: semilattice
 begin
 
-fun le_const where
-"_ \<sqsubseteq> Any = True" |
-"Const n \<sqsubseteq> Const m = (n=m)" |
-"Any \<sqsubseteq> Const _ = False"
+fun less_eq_const where
+"_ \<le> Any = True" |
+"Const n \<le> Const m = (n=m)" |
+"Any \<le> Const _ = False"
+
+definition "a < (b::const) = (a \<le> b & ~ b \<le> a)"
 
 fun join_const where
 "Const m \<squnion> Const n = (if n=m then Const m else Any)" |
@@ -36,17 +38,21 @@
 
 instance
 proof
-  case goal1 thus ?case by (cases x) simp_all
+  case goal1 thus ?case by (rule less_const_def)
+next
+  case goal2 show ?case by (cases x) simp_all
 next
-  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
+  case goal3 thus ?case by(cases z, cases y, cases x, simp_all)
 next
-  case goal3 thus ?case by(cases x, cases y, simp_all)
+  case goal4 thus ?case by(cases x, cases y, simp_all, cases y, simp_all)
 next
-  case goal4 thus ?case by(cases y, cases x, simp_all)
+  case goal6 thus ?case by(cases x, cases y, simp_all)
+next
+  case goal7 thus ?case by(cases y, cases x, simp_all)
 next
-  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
+  case goal8 thus ?case by(cases z, cases y, cases x, simp_all)
 next
-  case goal6 thus ?case by(simp add: Top_const_def)
+  case goal5 thus ?case by(simp add: top_const_def)
 qed
 
 end
@@ -58,7 +64,7 @@
   case goal1 thus ?case
     by(cases a, cases b, simp, simp, cases b, simp, simp)
 next
-  case goal2 show ?case by(simp add: Top_const_def)
+  case goal2 show ?case by(simp add: top_const_def)
 next
   case goal3 show ?case by simp
 next
@@ -74,7 +80,7 @@
 
 subsubsection "Tests"
 
-definition "steps c i = (step_const(top(vars c)) ^^ i) (bot c)"
+definition "steps c i = (step_const(Top(vars c)) ^^ i) (bot c)"
 
 value "show_acom (steps test1_const 0)"
 value "show_acom (steps test1_const 1)"
@@ -139,7 +145,7 @@
 next
   case goal2 thus ?case by(auto simp: m_const_def split: const.splits)
 next
-  case goal3 thus ?case by(auto simp: m_const_def split: const.splits)
+  case goal3 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
 qed
 
 thm AI_Some_measure