--- a/src/HOLCF/FOCUS/Fstream.thy Tue Oct 12 09:08:27 2010 -0700
+++ b/src/HOLCF/FOCUS/Fstream.thy Tue Oct 12 09:32:21 2010 -0700
@@ -95,7 +95,7 @@
apply (safe)
apply (erule_tac [!] contrapos_np)
prefer 2 apply (fast elim: DefE)
-apply (rule Lift_cases)
+apply (rule lift.exhaust)
apply (erule (1) notE)
apply (safe)
apply (drule Def_inject_less_eq [THEN iffD1])
--- a/src/HOLCF/Lift.thy Tue Oct 12 09:08:27 2010 -0700
+++ b/src/HOLCF/Lift.thy Tue Oct 12 09:32:21 2010 -0700
@@ -43,12 +43,6 @@
text {* @{term UU} and @{term Def} *}
-lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)"
- by (induct x) simp_all
-
-lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
- by (insert Lift_exhaust) blast
-
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
by (cases x) simp_all