src/HOL/Set.ML
changeset 3919 c036caebfc75
parent 3912 4ed64ad7fb42
child 3960 7a38fae985f9
     1.1 --- a/src/HOL/Set.ML	Fri Oct 17 15:23:14 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Oct 17 15:25:12 1997 +0200
     1.3 @@ -646,7 +646,7 @@
     1.4  
     1.5  
     1.6  (** Rewrite rules for boolean case-splitting: faster than 
     1.7 -	setloop split_tac[expand_if]
     1.8 +	addsplits[expand_if]
     1.9  **)
    1.10  
    1.11  bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
    1.12 @@ -669,7 +669,7 @@
    1.13  
    1.14  (*Not for Addsimps -- it can cause goals to blow up!*)
    1.15  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    1.16 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
    1.18  qed "mem_if";
    1.19  
    1.20  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;