changeset 3919 | c036caebfc75 |
parent 3590 | 4d307341d0af |
child 4089 | 96fba19bcbe2 |
--- a/src/HOL/ex/Recdef.ML Fri Oct 17 15:23:14 1997 +0200 +++ b/src/HOL/ex/Recdef.ML Fri Oct 17 15:25:12 1997 +0200 @@ -13,7 +13,7 @@ goal thy "(x mem qsort (ord,l)) = (x mem l)"; by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1); -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if]))); +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]))); by (Blast_tac 1); qed "qsort_mem_stable";