# HG changeset patch
# User lcp
# Date 754747525 -3600
# Node ID 17b6487e1ac786a6f509abda5c9ce8f34b78c067
# Parent  803ccc4a83bb3297e7bf609088bf85affe768595
HOL/llist/LList_corec_subset1: does not need induction

diff -r 803ccc4a83bb -r 17b6487e1ac7 LList.ML
--- 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();
 
diff -r 803ccc4a83bb -r 17b6487e1ac7 llist.ML
--- 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();