Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Addition of Finite as parent allows cardinality theorems
authorpaulson
Fri, 30 May 1997 15:21:53 +0200
changeset 3373 b19b1456cc78
parent 3372 6e472c8f0011
child 3374 182a2b76d19e
Addition of Finite as parent allows cardinality theorems
src/HOL/Integ/Equiv.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle