src/HOL/Set.ML
changeset 4686 74a12e86b20b
parent 4523 16f5efe9812d
child 4770 3e026ace28da
     1.1 --- a/src/HOL/Set.ML	Fri Mar 06 18:25:28 1998 +0100
     1.2 +++ b/src/HOL/Set.ML	Sat Mar 07 16:29:29 1998 +0100
     1.3 @@ -664,7 +664,7 @@
     1.4  
     1.5  (*Not for Addsimps -- it can cause goals to blow up!*)
     1.6  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
     1.7 -by (simp_tac (simpset() addsplits [expand_if]) 1);
     1.8 +by (Simp_tac 1);
     1.9  qed "mem_if";
    1.10  
    1.11  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;