--- a/src/HOL/Integ/Equiv.thy Thu Dec 06 00:39:40 2001 +0100
+++ b/src/HOL/Integ/Equiv.thy Thu Dec 06 00:40:04 2001 +0100
@@ -6,7 +6,7 @@
Equivalence relations in Higher-Order Set Theory
*)
-Equiv = Relation + Finite +
+Equiv = Relation + Finite_Set +
constdefs
equiv :: "['a set, ('a*'a) set] => bool"
"equiv A r == refl A r & sym(r) & trans(r)"
--- a/src/HOL/Wellfounded_Relations.thy Thu Dec 06 00:39:40 2001 +0100
+++ b/src/HOL/Wellfounded_Relations.thy Thu Dec 06 00:40:04 2001 +0100
@@ -10,12 +10,7 @@
separately.
*)
-Wellfounded_Relations = Finite +
-
-(* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
-instance unit :: finite (finite_unit)
-instance "*" :: (finite,finite) finite (finite_Prod)
-
+Wellfounded_Relations = Finite_Set +
constdefs
less_than :: "(nat*nat)set"