# HG changeset patch
# User paulson
# Date 993568022 -7200
# Node ID bad5995167306f1cce72cf9bcd0935841320e69f
# Parent  cde6edd51ff6ba0997c43114d4b5a15ebe59f17a
gave Greatest_le its proper name

diff -r cde6edd51ff6 -r bad599516730 src/HOL/GroupTheory/Exponent.ML
--- a/src/HOL/GroupTheory/Exponent.ML	Tue Jun 26 17:06:18 2001 +0200
+++ b/src/HOL/GroupTheory/Exponent.ML	Tue Jun 26 17:07:02 2001 +0200
@@ -258,7 +258,7 @@
 
 Goal "[|p^k dvd n;  p\\<in>prime;  0<n|] ==> k <= exponent p n";
 by (asm_full_simp_tac (simpset() addsimps [exponent_def]) 1); 
-by (etac GreatestM_nat_le 1);
+by (etac Greatest_le 1);
 by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 1);  
 qed_spec_mp "exponent_ge";
 
diff -r cde6edd51ff6 -r bad599516730 src/HOL/NatArith.ML
--- a/src/HOL/NatArith.ML	Tue Jun 26 17:06:18 2001 +0200
+++ b/src/HOL/NatArith.ML	Tue Jun 26 17:07:02 2001 +0200
@@ -182,7 +182,7 @@
      "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)";
 by (rtac GreatestM_nat_le 1); 
 by Auto_tac;  
-qed "GreatestM_nat_le";
+qed "Greatest_le";
 
 (*No analogue of not_less_Least or Least_Suc yet, since it isn't used much*)