src/HOL/Induct/LList.ML
changeset 3919 c036caebfc75
parent 3842 b55686a7b22c
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/Induct/LList.ML	Fri Oct 17 15:23:14 1997 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Fri Oct 17 15:25:12 1997 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  (** Simplification **)
     1.6  
     1.7 -simpset := !simpset setloop split_tac [expand_split, expand_sum_case];
     1.8 +simpset := !simpset addsplits [expand_split, expand_sum_case];
     1.9  
    1.10  (*For adding _eqI rules to a simpset; we must remove Pair_eq because
    1.11    it may turn an instance of reflexivity into a conjunction!*)
    1.12 @@ -68,11 +68,11 @@
    1.13  
    1.14  (*UNUSED; obsolete?
    1.15  goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
    1.16 -by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
    1.17 +by (simp_tac (!simpset addsplits [expand_split]) 1);
    1.18  qed "split_UN1";
    1.19  
    1.20  goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
    1.21 -by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
    1.22 +by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
    1.23  qed "sum_case2_UN1";
    1.24  *)
    1.25  
    1.26 @@ -310,7 +310,7 @@
    1.27  by (rename_tac "y" 1);
    1.28  by (stac prem1 1);
    1.29  by (stac prem2 1);
    1.30 -by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
    1.31 +by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
    1.32  by (strip_tac 1);
    1.33  by (res_inst_tac [("n", "n")] natE 1);
    1.34  by (rename_tac "m" 2);