changeset 14485 | ea2707645af8 |
parent 13735 | 7de9342aca7a |
--- a/src/HOL/SetInterval.ML Thu Mar 25 10:31:25 2004 +0100 +++ b/src/HOL/SetInterval.ML Thu Mar 25 10:32:21 2004 +0100 @@ -49,3 +49,7 @@ val lessThan_def = thm "lessThan_def"; val lessThan_iff = thm "lessThan_iff"; val single_Diff_lessThan = thm "single_Diff_lessThan"; + +val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite"; +val finite_atMost = thm "finite_atMost"; +val finite_lessThan = thm "finite_lessThan";