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.
new default rules
authorpaulson
Thu, 25 May 2000 15:13:57 +0200
changeset 8971 881853835a37
parent 8970 3ac901561f33
child 8972 b734bdb6042d
new default rules
src/HOL/Finite.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite.ML	Thu May 25 15:12:40 2000 +0200
+++ b/src/HOL/Finite.ML	Thu May 25 15:13:57 2000 +0200
@@ -224,6 +224,7 @@
 by (simp_tac (simpset() addsimps [atMost_Suc]) 2);
 by Auto_tac;
 qed "finite_atMost";
+AddIffs [finite_lessThan, finite_atMost];
 
 (* A bounded set of natural numbers is finite *)
 Goal "(!i:N. i<(n::nat)) ==> finite N";
isabelle