1 

     1 

     2 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}

     2 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}

     3 

     3 

     4 theory LarryInt 

     4 theory LarryInt 

     6 begin

     6 begin

     7 

     7 

     8 fun

     8 fun

     9   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 

     9   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 

    10 where

    10 where