doc-src/TutorialI/Sets/sets.tex
changeset 10372 d1bacec57f5e
parent 10341 6eb91805a012
child 10373 f9211fc8cd7d
equal deleted inserted replaced
10371:4015fdd0bcf0 10372:d1bacec57f5e
   631 \rulename{vimage_Compl}
   631 \rulename{vimage_Compl}
   632 \end{isabelle}
   632 \end{isabelle}
   633 
   633 
   634 
   634 
   635 \section{Relations}
   635 \section{Relations}
       
   636 \label{sec:Relations}
   636 
   637 
   637 A \textbf{relation} is a set of pairs.  As such, the set operations apply
   638 A \textbf{relation} is a set of pairs.  As such, the set operations apply
   638 to them.  For instance, we may form the union of two relations.  Other
   639 to them.  For instance, we may form the union of two relations.  Other
   639 primitives are defined specifically for relations. 
   640 primitives are defined specifically for relations. 
   640 
   641