src/HOL/Set.ML

 
 (*** Set reasoning tools ***)
 
 
 (** Rewrite rules for boolean case-splitting: faster than 
-	setloop split_tac[expand_if]
+	addsplits[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);
 

 		 UN_iff, UN1_iff, Union_iff, 
 		 INT_iff, INT1_iff, Inter_iff];
 
 (*Not for Addsimps -- it can cause goals to blow up!*)
 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
 qed "mem_if";
 
 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
 
 simpset := !simpset addcongs [ball_cong,bex_cong]