ex/InSort.ML

--- a/ex/InSort.ML	Fri Dec 02 11:43:20 1994 +0100
+++ b/ex/InSort.ML	Fri Dec 02 16:09:49 1994 +0100
@@ -20,27 +20,27 @@
 qed "transfD";
 
 goal InSort.thy "list_all(p,ins(f,x,xs)) = (list_all(p,xs) & p(x))";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(asm_simp_tac insort_ss 1);
 by(asm_simp_tac (insort_ss setloop (split_tac [expand_if])) 1);
 by(fast_tac HOL_cs 1);
 val insort_ss = insort_ss addsimps [result()];
 
 goal InSort.thy "(!x. p(x) --> q(x)) --> list_all(p,xs) --> list_all(q,xs)";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if]))));
 qed "list_all_imp";
 
 val prems = goal InSort.thy
   "[| total(f); transf(f) |] ==>  sorted(f,ins(f,x,xs)) = sorted(f,xs)";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if]))));
 by(cut_facts_tac prems 1);
-by(cut_inst_tac [("p","f(xa)"),("q","f(x)")] list_all_imp 1);
+by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1);
 by(fast_tac (HOL_cs addDs [totalD,transfD]) 1);
 val insort_ss = insort_ss addsimps [result()];
 
 goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted(f,insort(f,xs))";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac insort_ss));
 result();