src/ZF/upair.thy

 (*  Title:      ZF/upair.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Observe the order of dependence:
     Upair is defined in terms of Replace

 lemma split_if [split]:
      "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
 by (case_tac Q, simp_all)
 
 (** Rewrite rules for boolean case-splitting: faster than 
-	addsplits[split_if]
+        addsplits[split_if]
 **)
 
 lemmas split_if_eq1 = split_if [of "%x. x = b", standard]
 lemmas split_if_eq2 = split_if [of "%x. a = x", standard]