src/HOL/Integ/Equiv.thy
changeset 3373 b19b1456cc78
parent 2215 ebf910e7ec87
child 6812 ac4c9707ae53
equal deleted inserted replaced
3372:6e472c8f0011 3373:b19b1456cc78
     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*)