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.
renamed real_of_nat_eq_cancel to real_of_nat_inject, and declared as iff rule;
authorwenzelm
Thu, 27 Sep 2001 18:46:32 +0200
changeset 11599 12cc28aafb4d
parent 11598 4f26832a7b86
child 11600 bbd6268e0b4b
renamed real_of_nat_eq_cancel to real_of_nat_inject, and declared as iff rule;
src/HOL/Real/RealOrd.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Real/RealOrd.ML	Thu Sep 27 18:45:40 2001 +0200
+++ b/src/HOL/Real/RealOrd.ML	Thu Sep 27 18:46:32 2001 +0200
@@ -360,8 +360,8 @@
 
 Goal "(real (n::nat) = real m) = (n = m)";
 by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
-qed "real_of_nat_eq_cancel";
-Addsimps [real_of_nat_eq_cancel];
+qed "real_of_nat_inject";
+AddIffs [real_of_nat_inject];
 
 Goal "n <= m --> real (m - n) = real (m::nat) - real n";
 by (induct_tac "m" 1);
@@ -371,7 +371,7 @@
 qed_spec_mp "real_of_nat_diff";
 
 Goal "(real (n::nat) = 0) = (n = 0)";
-by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset()));
+by (auto_tac ((claset() addIs [inj_real_of_nat RS injD], simpset()) delIffs [real_of_nat_inject]));
 qed "real_of_nat_zero_iff";
 
 Goal "neg z ==> real (nat z) = 0";
isabelle