--- a/src/HOL/ex/InSort.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/InSort.ML Fri Jun 21 12:18:50 1996 +0200
@@ -8,19 +8,19 @@
goalw InSort.thy [Sorting.total_def]
"!!f. [| total(f); ~f x y |] ==> f y x";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
qed "totalD";
goalw InSort.thy [Sorting.transf_def]
"!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
qed "transfD";
goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))";
by(list.induct_tac "xs" 1);
by(Asm_simp_tac 1);
by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
Addsimps [result()];
goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs";
@@ -34,7 +34,7 @@
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
by(cut_facts_tac prems 1);
by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1);
-by(fast_tac (HOL_cs addDs [totalD,transfD]) 1);
+by(fast_tac (!claset addDs [totalD,transfD]) 1);
Addsimps [result()];
goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)";