# HG changeset patch
# User paulson
# Date 864998513 -7200
# Node ID b19b1456cc7889e5fb554cb374bffb6c171e24d0
# Parent  6e472c8f001130599845f80ce27551bbf7d7f0f9
Addition of Finite as parent allows cardinality theorems

diff -r 6e472c8f0011 -r b19b1456cc78 src/HOL/Integ/Equiv.thy
--- 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"