src/HOL/ex/Sorting.ML
changeset 4089 96fba19bcbe2
parent 4069 d6d06a03a2e9
child 4686 74a12e86b20b
--- a/src/HOL/ex/Sorting.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/ex/Sorting.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -8,20 +8,20 @@
 
 goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
+by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
 qed "mset_append";
 
 goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
 \                     mset xs x";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
+by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
 qed "mset_compl_add";
 
 Addsimps [mset_append, mset_compl_add];
 
 goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
+by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
 by (Fast_tac 1);
 qed "set_via_mset";
 
@@ -30,7 +30,7 @@
 val prems = goalw Sorting.thy [transf_def]
   "transf(le) ==> sorted1 le xs = sorted le xs";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsplits [split_list_case])));
+by (ALLGOALS(asm_simp_tac (simpset() addsplits [split_list_case])));
 by (cut_facts_tac prems 1);
 by (Fast_tac 1);
 qed "sorted1_is_sorted";