src/HOL/Equiv_Relations.thy
changeset 29655 ac31940cfb69
parent 28562 4e74209f113e
child 30198 922f944f03b2
     1.1 --- a/src/HOL/Equiv_Relations.thy	Wed Jan 28 11:03:16 2009 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Wed Jan 28 11:03:42 2009 +0100
     1.3 @@ -1,12 +1,11 @@
     1.4 -(*  ID:         $Id$
     1.5 -    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 +(*  Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1996  University of Cambridge
     1.8  *)
     1.9  
    1.10  header {* Equivalence Relations in Higher-Order Set Theory *}
    1.11  
    1.12  theory Equiv_Relations
    1.13 -imports Finite_Set Relation
    1.14 +imports Finite_Set Relation Plain
    1.15  begin
    1.16  
    1.17  subsection {* Equivalence relations *}