# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257327813 -3600
# Node ID 34ad627ac5d5696448ffb3c069a9603108395c01
# Parent  df225aa45770778a091e5e4bd2f1940bd4195308
fixed definition of PLUS

diff -r df225aa45770 -r 34ad627ac5d5 IntEx.thy
--- a/IntEx.thy	Wed Nov 04 10:31:20 2009 +0100
+++ b/IntEx.thy	Wed Nov 04 10:43:33 2009 +0100
@@ -39,7 +39,7 @@
 quotient_def 
   PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
-  "PLUS x y \<equiv> my_plus x y"
+  "PLUS \<equiv> my_plus"
 
 term PLUS
 thm PLUS_def
diff -r df225aa45770 -r 34ad627ac5d5 QuotMain.thy
--- a/QuotMain.thy	Wed Nov 04 10:31:20 2009 +0100
+++ b/QuotMain.thy	Wed Nov 04 10:43:33 2009 +0100
@@ -1014,6 +1014,7 @@
   end
 *}
 
+
 ML {*
 fun lift_thm lthy qty qty_name rsp_thms defs t = let
   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;