# HG changeset patch
# User paulson
# Date 1072187123 -3600
# Node ID 255190be18c01085a1c44d8579e3b9c087368303
# Parent  7dbd3988b15b68d971904baee9525441305c1b01
renaming some theorems

diff -r 7dbd3988b15b -r 255190be18c0 src/HOL/Hyperreal/NthRoot.ML
--- a/src/HOL/Hyperreal/NthRoot.ML	Tue Dec 23 12:54:45 2003 +0100
+++ b/src/HOL/Hyperreal/NthRoot.ML	Tue Dec 23 14:45:23 2003 +0100
@@ -85,7 +85,7 @@
 \    isLub (UNIV::real set) \
 \    {x. x ^ n <= a & 0 < x} u |] ==> a <= u ^ n";
 by (ftac lemma_nth_realpow_isLub_ge 1 THEN Step_tac 1);
-by (rtac (LIMSEQ_inverse_real_of_posnat_add RS LIMSEQ_pow 
+by (rtac (LIMSEQ_inverse_real_of_nat_add RS LIMSEQ_pow 
     RS LIMSEQ_le_const) 1);
 by (auto_tac (claset(),simpset() addsimps [real_of_nat_def,
     real_of_posnat_Suc]));
@@ -133,7 +133,7 @@
 \    isLub (UNIV::real set) \
 \    {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a";
 by (ftac lemma_nth_realpow_isLub_le 1 THEN Step_tac 1);
-by (rtac (LIMSEQ_inverse_real_of_posnat_add_minus_mult RS LIMSEQ_pow 
+by (rtac (LIMSEQ_inverse_real_of_nat_add_minus_mult RS LIMSEQ_pow 
     RS LIMSEQ_le_const2) 1);
 by (auto_tac (claset(),simpset() addsimps [real_of_nat_def,real_of_posnat_Suc]));
 qed "realpow_nth_le";
diff -r 7dbd3988b15b -r 255190be18c0 src/HOL/Hyperreal/SEQ.ML
--- a/src/HOL/Hyperreal/SEQ.ML	Tue Dec 23 12:54:45 2003 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML	Tue Dec 23 14:45:23 2003 +0100
@@ -1168,12 +1168,12 @@
 by (cut_facts_tac
     [ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1);
 by Auto_tac;
-qed "LIMSEQ_inverse_real_of_posnat_add";
+qed "LIMSEQ_inverse_real_of_nat_add";
 
 Goal "(%n. r + inverse(real(Suc n))) ----NS> r";
 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-    LIMSEQ_inverse_real_of_posnat_add]) 1);
-qed "NSLIMSEQ_inverse_real_of_posnat_add";
+    LIMSEQ_inverse_real_of_nat_add]) 1);
+qed "NSLIMSEQ_inverse_real_of_nat_add";
 
 (*--------------
     Also...
@@ -1183,23 +1183,23 @@
 by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat]
                    MRS LIMSEQ_add_minus] 1);
 by (Auto_tac);
-qed "LIMSEQ_inverse_real_of_posnat_add_minus";
+qed "LIMSEQ_inverse_real_of_nat_add_minus";
 
 Goal "(%n. r + -inverse(real(Suc n))) ----NS> r";
 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-    LIMSEQ_inverse_real_of_posnat_add_minus]) 1);
-qed "NSLIMSEQ_inverse_real_of_posnat_add_minus";
+    LIMSEQ_inverse_real_of_nat_add_minus]) 1);
+qed "NSLIMSEQ_inverse_real_of_nat_add_minus";
 
 Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r";
 by (cut_inst_tac [("b","1")] ([LIMSEQ_const,
-    LIMSEQ_inverse_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1);
+    LIMSEQ_inverse_real_of_nat_add_minus] MRS LIMSEQ_mult) 1);
 by (Auto_tac);
-qed "LIMSEQ_inverse_real_of_posnat_add_minus_mult";
+qed "LIMSEQ_inverse_real_of_nat_add_minus_mult";
 
 Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r";
 by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-    LIMSEQ_inverse_real_of_posnat_add_minus_mult]) 1);
-qed "NSLIMSEQ_inverse_real_of_posnat_add_minus_mult";
+    LIMSEQ_inverse_real_of_nat_add_minus_mult]) 1);
+qed "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
 
 (*---------------------------------------------------------------
                           Real Powers