src/HOLCF/Lift3.ML

--- a/src/HOLCF/Lift3.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Lift3.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -94,12 +94,6 @@
 by (fast_tac (HOL_cs addSEs prems) 1);
 qed"Lift_cases";
 
-goal thy
-  "P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
-by (lift.induct_tac "x" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "expand_lift_case";
-
 goal thy "(x~=UU)=(? y. x=Def y)";
 by (rtac iffI 1);
 by (rtac Lift_cases 1);