diff -r fc48fe9667f2 -r 2da4fb1894d2 IntEx2.thy --- a/IntEx2.thy Sun Dec 06 22:57:44 2009 +0100 +++ b/IntEx2.thy Sun Dec 06 22:58:03 2009 +0100 @@ -6,6 +6,7 @@ ("Tools/int_arith.ML") begin + fun intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) where