| changeset 8971 | 881853835a37 |
| parent 8963 | 0d4abacae6aa |
| child 8981 | fe1f3d52e027 |
--- 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";