# HG changeset patch
# User wenzelm
# Date 1007595604 -3600
# Node ID 9c27f28c8f5a73e2c803b8ed5dfeea33fa6039b3
# Parent  6766aa05e4eb394660c5eb8b7c904641de00aa37
renamed Finite to Finite_Set;

diff -r 6766aa05e4eb -r 9c27f28c8f5a src/HOL/Integ/Equiv.thy
--- 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)"
diff -r 6766aa05e4eb -r 9c27f28c8f5a src/HOL/Wellfounded_Relations.thy
--- 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"