# HG changeset patch
# User huffman
# Date 1120783362 -7200
# Node ID e05c8039873a7cf3d092f06ff4c74332a4e9c6f8
# Parent  fd02f9d06e43ac6451035f5a4b16a2794a5f58ae
simplified proof of ifte_thms, removed ifte_simp

diff -r fd02f9d06e43 -r e05c8039873a src/HOLCF/Tr.ML
--- 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";
diff -r fd02f9d06e43 -r e05c8039873a src/HOLCF/Tr.thy
--- 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"