# HG changeset patch
# User huffman
# Date 1120765268 -7200
# Node ID c96aaaf25f48e9ee00640e38e1e295e169f2eaca
# Parent  58b9ce4fac54db88b632e186d155b81ddebf4f3c
removed obsolete continuity theorems

diff -r 58b9ce4fac54 -r c96aaaf25f48 src/HOLCF/Lift.ML
--- a/src/HOLCF/Lift.ML	Thu Jul 07 21:22:15 2005 +0200
+++ b/src/HOLCF/Lift.ML	Thu Jul 07 21:41:08 2005 +0200
@@ -27,7 +27,7 @@
 val cont_flift1_arg = thm "cont_flift1_arg";
 val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg";
 val cont_flift1_not_arg = thm "cont_flift1_not_arg";
-val cont_flift2_arg = thm "cont_flift2_arg";
+(*val cont_flift2_arg = thm "cont_flift2_arg";*)
 val cont_if = thm "cont_if";
 val flift1_Def = thm "flift1_Def";
 val flift1_strict = thm "flift1_strict";
diff -r 58b9ce4fac54 -r c96aaaf25f48 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Thu Jul 07 21:22:15 2005 +0200
+++ b/src/HOLCF/Lift.thy	Thu Jul 07 21:41:08 2005 +0200
@@ -193,18 +193,11 @@
   apply (rule cont_flift1_arg)
   done
 
-lemma cont_flift2_arg: "cont (lift_case UU (%y. Def (f y)))"
-  -- {* @{text flift2} is continuous in its argument itself. *}
-  apply (rule flatdom_strict2cont)
-  apply simp
-  done
-
 text {*
   \medskip Extension of @{text cont_tac} and installation of simplifier.
 *}
 
 lemmas cont_lemmas_ext [simp] =
-  cont_flift1_arg cont_flift2_arg
   cont_flift1_arg_and_not_arg cont2cont_lambda
   cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
 
@@ -214,9 +207,9 @@
 fun cont_tac  i = resolve_tac cont_lemmas2 i;
 fun cont_tacR i = REPEAT (cont_tac i);
 
-local val flift1_def = thm "flift1_def" and flift2_def = thm "flift2_def"
+local val flift1_def = thm "flift1_def"
 in fun cont_tacRs i =
-  simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN
+  simp_tac (simpset() addsimps [flift1_def]) i THEN
   REPEAT (cont_tac i)
 end;
 *}