Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gave Greatest_le its proper name
authorpaulson
Tue, 26 Jun 2001 17:07:02 +0200
changeset 11385 bad599516730
parent 11384 cde6edd51ff6
child 11386 cf8d81cf8034
gave Greatest_le its proper name
src/HOL/GroupTheory/Exponent.ML file | annotate | diff | comparison | revisions
src/HOL/NatArith.ML file | annotate | diff | comparison | revisions 
--- 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";
 
--- 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*)
isabelle