src/HOL/Integ/Equiv.thy
changeset 3373 b19b1456cc78
parent 2215 ebf910e7ec87
child 6812 ac4c9707ae53
--- a/src/HOL/Integ/Equiv.thy	Fri May 30 15:21:21 1997 +0200
+++ b/src/HOL/Integ/Equiv.thy	Fri May 30 15:21:53 1997 +0200
@@ -6,7 +6,7 @@
 Equivalence relations in Higher-Order Set Theory 
 *)
 
-Equiv = Relation +
+Equiv = Relation + Finite + 
 consts
     refl,equiv  ::      "['a set,('a*'a) set]=>bool"
     sym         ::      "('a*'a) set=>bool"