equal
deleted
inserted
replaced
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 Equivalence relations in Higher-Order Set Theory |
6 Equivalence relations in Higher-Order Set Theory |
7 *) |
7 *) |
8 |
8 |
9 Equiv = Relation + |
9 Equiv = Relation + Finite + |
10 consts |
10 consts |
11 refl,equiv :: "['a set,('a*'a) set]=>bool" |
11 refl,equiv :: "['a set,('a*'a) set]=>bool" |
12 sym :: "('a*'a) set=>bool" |
12 sym :: "('a*'a) set=>bool" |
13 "'/" :: "['a set,('a*'a) set]=>'a set set" (infixl 90) |
13 "'/" :: "['a set,('a*'a) set]=>'a set set" (infixl 90) |
14 (*set of equiv classes*) |
14 (*set of equiv classes*) |