# HG changeset patch
# User paulson
# Date 959260437 -7200
# Node ID 881853835a37084d9bcad57555025b03f2c48ff1
# Parent  3ac901561f335d937e4c7ebc132915b6db18467d
new default rules

diff -r 3ac901561f33 -r 881853835a37 src/HOL/Finite.ML
--- 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";