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.
Adding lessI to default claset
authorpaulson
Thu, 07 Nov 1996 10:11:06 +0100
changeset 2164 c87368fc736b
parent 2163 4d43e7486164
child 2165 63dfe7f19cad
Adding lessI to default claset
src/HOL/Nat.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nat.ML	Wed Nov 06 12:49:31 1996 +0100
+++ b/src/HOL/Nat.ML	Thu Nov 07 10:11:06 1996 +0100
@@ -215,7 +215,7 @@
 goalw Nat.thy [less_def] "n < Suc(n)";
 by (rtac (pred_natI RS r_into_trancl) 1);
 qed "lessI";
-Addsimps [lessI];
+AddIffs [lessI];
 
 (* i<j ==> i<Suc(j) *)
 val less_SucI = lessI RSN (2, less_trans);
isabelle