tuned

--- a/src/HOLCF/Lift.thy	Fri Jun 20 17:56:00 2008 +0200
+++ b/src/HOLCF/Lift.thy	Fri Jun 20 17:58:16 2008 +0200
@@ -73,23 +73,21 @@
 lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
   by simp
 
-lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y = (x = y)"
+lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
 by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def)
 
-lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)"
-apply (induct y)
-apply simp
-apply (simp add: Def_inject_less_eq)
-done
+lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
+by (induct y, simp, simp add: Def_inject_less_eq)
 
 
 subsection {* Lift is flat *}
 
-lemma less_lift: "(x::'a lift) \<sqsubseteq> y = (x = y \<or> x = \<bottom>)"
-by (induct x, simp_all)
-
 instance lift :: (type) flat
-by (intro_classes, auto simp add: less_lift)
+proof
+  fix x y :: "'a lift"
+  assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
+    by (induct x) auto
+qed
 
 text {*
   \medskip Two specific lemmas for the combination of LCF and HOL
@@ -133,7 +131,7 @@
 done
 
 lemma cont_flift1: "cont flift1"
-apply (unfold flift1_def)
+unfolding flift1_def
 apply (rule cont2cont_LAM)
 apply (rule cont_lift_case2)
 apply (rule cont_lift_case1)

--- a/src/HOLCF/Porder.thy	Fri Jun 20 17:56:00 2008 +0200
+++ b/src/HOLCF/Porder.thy	Fri Jun 20 17:58:16 2008 +0200
@@ -326,7 +326,7 @@
 
 lemma bin_chainmax:
   "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
-by (unfold max_in_chain_def, simp)
+unfolding max_in_chain_def by simp
 
 lemma lub_bin_chain:
   "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"