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()));