simplified proof of ifte_thms, removed ifte_simp

--- a/src/HOLCF/Tr.ML	Fri Jul 08 02:42:04 2005 +0200
+++ b/src/HOLCF/Tr.ML	Fri Jul 08 02:42:42 2005 +0200
@@ -13,7 +13,6 @@
 val tr_defs = thms "tr_defs";
 val dist_less_tr = thms "dist_less_tr";
 val dist_eq_tr = thms "dist_eq_tr";
-val ifte_simp = thm "ifte_simp";
 val ifte_thms = thms "ifte_thms";
 val andalso_thms = thms "andalso_thms";
 val orelse_thms = thms "orelse_thms";

--- a/src/HOLCF/Tr.thy	Fri Jul 08 02:42:04 2005 +0200
+++ b/src/HOLCF/Tr.thy	Fri Jul 08 02:42:42 2005 +0200
@@ -84,18 +84,11 @@
 
 text {* lemmas about andalso, orelse, neg and if *}
 
-lemma ifte_simp:
-  "If x then e1 else e2 fi =
-    flift1 (%b. if b then e1 else e2)$x"
-apply (unfold ifte_def TT_def FF_def flift1_def)
-apply (simp add: cont_flift1_arg cont_if)
-done
-
 lemma ifte_thms [simp]:
   "If UU then e1 else e2 fi = UU"
   "If FF then e1 else e2 fi = e2"
   "If TT then e1 else e2 fi = e1"
-by (simp_all add: ifte_simp TT_def FF_def)
+by (simp_all add: ifte_def TT_def FF_def)
 
 lemma andalso_thms [simp]:
   "(TT andalso y) = y"