diff -r 0165b805fe09 -r 4ed64ad7fb42 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Oct 17 10:58:44 1997 +0200
+++ b/src/HOL/Set.ML	Fri Oct 17 11:00:00 1997 +0200
@@ -645,6 +645,22 @@
 (*** Set reasoning tools ***)
 
 
+(** Rewrite rules for boolean case-splitting: faster than 
+	setloop split_tac[expand_if]
+**)
+
+bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
+bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if);
+
+bind_thm ("expand_if_mem1", 
+    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] expand_if);
+bind_thm ("expand_if_mem2", 
+    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if);
+
+val expand_ifs = [if_bool_eq, expand_if_eq1, expand_if_eq2,
+		  expand_if_mem1, expand_if_mem2];
+
+
 (*Each of these has ALREADY been added to !simpset above.*)
 val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
                  mem_Collect_eq,