src/HOL/Hyperreal/SEQ.ML
 changeset 14378 69c4d5997669 parent 14371 c78c7da09519 child 14387 e96d5c42c4b0
```     1.1 --- a/src/HOL/Hyperreal/SEQ.ML	Thu Feb 05 10:45:28 2004 +0100
1.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Tue Feb 10 12:02:11 2004 +0100
1.3 @@ -4,6 +4,8 @@
1.4      Description : Theory of sequence and series of real numbers
1.5  *)
1.6
1.7 +val Nats_1 = thm"Nats_1";
1.8 +
1.9  fun CLAIM_SIMP str thms =
1.10                 prove_goal (the_context()) str
1.11                 (fn prems => [cut_facts_tac prems 1,
1.12 @@ -92,7 +94,7 @@
1.13  by (induct_tac "u" 1);
1.14  by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
1.15  by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
1.16 -    finite_nat_le_segment], simpset()));
1.17 +    rewrite_rule [atMost_def] finite_atMost], simpset()));
1.18  by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
1.19  by (ALLGOALS(Asm_simp_tac));
1.20  qed "NSLIMSEQ_finite_set";
1.21 @@ -1050,7 +1052,7 @@
1.22       simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
1.23  by (dtac bspec 1 THEN assume_tac 1);
1.24  by (dtac bspec 1 THEN assume_tac 1);
1.25 -by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1);
1.26 +by (dtac (Nats_1 RSN (2,HNatInfinite_SHNat_add)) 1);
1.27  by (blast_tac (claset() addIs [approx_trans3]) 1);
1.28  qed "NSLIMSEQ_Suc";
1.29
1.30 @@ -1067,7 +1069,7 @@
1.31        simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
1.32  by (dtac bspec 1 THEN assume_tac 1);
1.33  by (dtac bspec 1 THEN assume_tac 1);
1.34 -by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
1.35 +by (ftac (Nats_1 RSN (2,HNatInfinite_SHNat_diff)) 1);
1.36  by (rotate_tac 2 1);
1.37  by (auto_tac (claset() addSDs [bspec] addIs [approx_trans3],
1.38      simpset()));
```