1.1 --- a/src/ZF/upair.ML	Fri Oct 17 11:00:50 1997 +0200
     1.2 +++ b/src/ZF/upair.ML	Fri Oct 17 11:09:34 1997 +0200
     1.3 @@ -261,6 +261,20 @@
     1.4             (Asm_simp_tac 1),
     1.5             (Asm_simp_tac 1) ]);
     1.6  
     1.7 +(** Rewrite rules for boolean case-splitting: faster than 
     1.8 +	setloop split_tac[expand_if]
     1.9 +**)
    1.10 +
    1.11 +bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
    1.12 +bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if);
    1.13 +
    1.14 +bind_thm ("expand_if_mem1", read_instantiate [("P", "%x. x : ?b")] expand_if);
    1.15 +bind_thm ("expand_if_mem2", read_instantiate [("P", "%x. ?a : x")] expand_if);
    1.16 +
    1.17 +val expand_ifs = [expand_if_eq1, expand_if_eq2,
    1.18 +		  expand_if_mem1, expand_if_mem2];
    1.19 +
    1.20 +(*Logically equivalent to expand_if_mem2*)
    1.21  qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
    1.22   (fn _=> [ (simp_tac (!simpset setloop split_tac [expand_if]) 1) ]);
    1.23