# HG changeset patch
# User paulson
# Date 932027640 -7200
# Node ID d6a721e7125df0c220df7867e1891abc23c9d183
# Parent  6def5ce146e23266602c1628ae99178da6309b05
more renaming of theorems from _nat to _int (corresponding to a function that
was similarly renamed some time ago

diff -r 6def5ce146e2 -r d6a721e7125d src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Thu Jul 15 10:33:16 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Thu Jul 15 10:34:00 1999 +0200
@@ -205,14 +205,14 @@
 
 Goalw [nat_def] "nat(int n) = n";
 by Auto_tac;
-qed "nat_nat";
+qed "nat_int";
 
 Goalw [nat_def] "nat(- int n) = 0";
 by (auto_tac (claset(),
 	      simpset() addsimps [neg_eq_less_int0, zminus_zless])); 
-qed "nat_zminus_nat";
+qed "nat_zminus_int";
 
-Addsimps [nat_nat, nat_zminus_nat];
+Addsimps [nat_int, nat_zminus_int];
 
 Goal "~ neg z ==> int (nat z) = z"; 
 by (dtac (not_neg_eq_ge_int0 RS iffD1) 1); 
@@ -245,12 +245,12 @@
 by (auto_tac (claset(), 
 	      simpset() addsimps [order_le_less, neg_eq_less_int0, 
 				  zle_def, neg_nat])); 
-qed "nat_le_0"; 
+qed "nat_le_int0"; 
 
 Goal "(nat w < nat z) = (int 0 < z & w < z)";
 by (case_tac "int 0 < z" 1);
 by (auto_tac (claset(), 
-	      simpset() addsimps [lemma, nat_le_0, linorder_not_less])); 
+	      simpset() addsimps [lemma, nat_le_int0, linorder_not_less])); 
 qed "zless_nat_conj";