--- a/LList.ML Tue Nov 30 17:44:04 1993 +0100
+++ b/LList.ML Wed Dec 01 13:05:25 1993 +0100
@@ -99,8 +99,8 @@
"LList_corec(a,f) <= case(f(a), %u.NIL, \
\ %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
by (rtac UN1_least 1);
-by (nat_ind_tac "k" 1);
-by (ALLGOALS(simp_tac corec_fun_ss));
+by (res_inst_tac [("n","k")] natE 1);
+by (ALLGOALS (asm_simp_tac corec_fun_ss));
by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
val LList_corec_subset1 = result();
--- a/llist.ML Tue Nov 30 17:44:04 1993 +0100
+++ b/llist.ML Wed Dec 01 13:05:25 1993 +0100
@@ -99,8 +99,8 @@
"LList_corec(a,f) <= case(f(a), %u.NIL, \
\ %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
by (rtac UN1_least 1);
-by (nat_ind_tac "k" 1);
-by (ALLGOALS(simp_tac corec_fun_ss));
+by (res_inst_tac [("n","k")] natE 1);
+by (ALLGOALS (asm_simp_tac corec_fun_ss));
by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
val LList_corec_subset1 = result();