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.
Suc_less_eq now with AddIffs. How could this have been overlooked?
authorpaulson
Wed, 22 Mar 2000 13:22:39 +0100
changeset 8555 17325ee838ab
parent 8554 ba33995b87ff
child 8556 52ef986bd0a6
Suc_less_eq now with AddIffs. How could this have been overlooked?
src/HOL/NatDef.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/NatDef.ML	Wed Mar 22 13:22:11 2000 +0100
+++ b/src/HOL/NatDef.ML	Wed Mar 22 13:22:39 2000 +0100
@@ -276,7 +276,7 @@
 Goal "(Suc(m) < Suc(n)) = (m<n)";
 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
 qed "Suc_less_eq";
-Addsimps [Suc_less_eq];
+AddIffs [Suc_less_eq];
 
 (*Goal "~(Suc(n) < n)";
 by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1);
isabelle