src/ZF/equalities.thy

 (*  Title:      ZF/equalities.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
 
-header{*Basic Equalities and Inclusions*}
+section{*Basic Equalities and Inclusions*}
 
 theory equalities imports pair begin
 
 text{*These cover union, intersection, converse, domain, range, etc.  Philippe
 de Groote proved many of the inclusions.*}