src/ZF/upair.thy

--- a/src/ZF/upair.thy	Tue Aug 19 13:53:58 2003 +0200
+++ b/src/ZF/upair.thy	Tue Aug 19 13:54:20 2003 +0200
@@ -223,8 +223,7 @@
 
 lemma split_if [split]:
      "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
-(*no case_tac yet!*)
-by (rule_tac P=Q in case_split_thm, simp_all)
+by (case_tac Q, simp_all)
 
 (** Rewrite rules for boolean case-splitting: faster than 
 	addsplits[split_if]