src/ZF/upair.thy

--- a/src/ZF/upair.thy	Wed Nov 23 22:07:55 2011 +0100
+++ b/src/ZF/upair.thy	Wed Nov 23 22:59:39 2011 +0100
@@ -224,8 +224,7 @@
      "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]
+(** Rewrite rules for boolean case-splitting: faster than split_if [split]
 **)
 
 lemmas split_if_eq1 = split_if [of "%x. x = b"] for b