# HG changeset patch
# User lcp
# Date 797163460 -7200
# Node ID 6a402dc505cfac4cb9de58f5773bd4afefaafb3b
# Parent  2317b680fe586f13e8b3a30a0fd65576b7f488cc
Proved if_iff and used it to simplify proof of if_type.

diff -r 2317b680fe58 -r 6a402dc505cf src/ZF/upair.ML
--- a/src/ZF/upair.ML	Thu Apr 06 12:15:27 1995 +0200
+++ b/src/ZF/upair.ML	Thu Apr 06 12:17:40 1995 +0200
@@ -241,11 +241,13 @@
 	   (asm_simp_tac if_ss 1),
 	   (asm_simp_tac if_ss 1) ]);
 
-val prems = goal ZF.thy
-    "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A";
-by (excluded_middle_tac "P" 1);
-by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
-qed "if_type";
+qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
+ (fn _=> [ (simp_tac (if_ss setloop split_tac [expand_if]) 1) ]);
+
+qed_goal "if_type" ZF.thy
+    "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A"
+ (fn prems=> [ (simp_tac 
+		(if_ss addsimps prems setloop split_tac [expand_if]) 1) ]);
 
 
 (*** Foundation lemmas ***)