--- a/IntEx.thy Thu Dec 03 13:59:53 2009 +0100 +++ b/IntEx.thy Thu Dec 03 14:00:43 2009 +0100 @@ -1,6 +1,7 @@ theory IntEx imports QuotMain begin + fun intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)