src/HOL/Induct/LFilter.ML

--- a/src/HOL/Induct/LFilter.ML	Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/LFilter.ML	Fri Oct 17 15:25:12 1997 +0200
@@ -96,7 +96,7 @@
 
 goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
 by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
-                           setloop split_tac[expand_if]) 1);
+                           addsplits [expand_if]) 1);
 qed "find_LCons";
 
 
@@ -141,7 +141,7 @@
 goal thy "lfilter p (LCons x l) = \
 \         (if p x then LCons x (lfilter p l) else lfilter p l)";
 by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
-                           setloop split_tac[expand_if]) 1);
+                           addsplits [expand_if]) 1);
 qed "lfilter_LCons";
 
 AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
@@ -186,7 +186,7 @@
 
 goal thy "lfilter p (lfilter p l) = lfilter p l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
+by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
 by Safe_tac;
 (*Cases: p x is true or false*)
 by (Blast_tac 1);
@@ -244,7 +244,7 @@
 \              ==> l'' = LCons y l' --> \
 \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
 by (etac findRel.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
 by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
 qed_spec_mp "findRel_conj_lfilter";
 
@@ -288,7 +288,7 @@
 
 goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
+by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
 by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
 qed "lfilter_conj";
 
@@ -326,7 +326,7 @@
 
 goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
+by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
 by Safe_tac;
 by (Blast_tac 1);
 by (case_tac "lmap f l : Domain (findRel p)" 1);