# HG changeset patch
# User huffman
# Date 1286901141 25200
# Node ID f2c78550c0b7ac1b1aab32e712b83df36445050e
# Parent  58ead6f77f8e00271cc7853c45d69d39f7162c96
remove unneeded lemmas Lift_exhaust, Lift_cases

diff -r 58ead6f77f8e -r f2c78550c0b7 src/HOLCF/FOCUS/Fstream.thy
--- 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])
diff -r 58ead6f77f8e -r f2c78550c0b7 src/HOLCF/Lift.thy
--- 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