# HG changeset patch
# User nipkow
# Date 1325532321 -3600
# Node ID 629aaafd3af6ebaf32ad041016f840f0a3502a63
# Parent  86e6e9d42ad7abc1ae823397959cfd2fa441941a
tuned

diff -r 86e6e9d42ad7 -r 629aaafd3af6 src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Mon Jan 02 15:15:46 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Mon Jan 02 20:25:21 2012 +0100
@@ -113,7 +113,7 @@
 
 subsubsection "Lifting"
 
-instantiation option :: (SL_top)SL_top
+instantiation option :: (preord)preord
 begin
 
 fun le_option where
@@ -127,6 +127,18 @@
 lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y & x \<sqsubseteq> y)"
 by (cases u) auto
 
+instance proof
+  case goal1 show ?case by(cases x, simp_all)
+next
+  case goal2 thus ?case
+    by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
+qed
+
+end
+
+instantiation option :: (SL_top)SL_top
+begin
+
 fun join_option where
 "Some x \<squnion> Some y = Some(x \<squnion> y)" |
 "None \<squnion> y = y" |
@@ -138,18 +150,13 @@
 definition "\<top> = Some \<top>"
 
 instance proof
-  case goal1 show ?case by(cases x, simp_all)
+  case goal1 thus ?case by(cases x, simp, cases y, simp_all)
 next
-  case goal2 thus ?case
-    by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
+  case goal2 thus ?case by(cases y, simp, cases x, simp_all)
 next
-  case goal3 thus ?case by(cases x, simp, cases y, simp_all)
-next
-  case goal4 thus ?case by(cases y, simp, cases x, simp_all)
+  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
 next
-  case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
-next
-  case goal6 thus ?case by(cases x, simp_all add: Top_option_def)
+  case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
 qed
 
 end