# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264492555 -3600
# Node ID e812f58fd1284b80296ba19fd4bc589a91f33a33
# Parent  44c92eaa4fad6c22705bfbd2d93554a7e52491fb
continued

diff -r 44c92eaa4fad -r e812f58fd128 Quot/QuotSum.thy
--- a/Quot/QuotSum.thy	Tue Jan 26 08:09:22 2010 +0100
+++ b/Quot/QuotSum.thy	Tue Jan 26 08:55:55 2010 +0100
@@ -76,17 +76,15 @@
   apply(blast)+
   done
 
-lemma sum_map_id[id_simps]: 
-  shows "sum_map id id \<equiv> id"
-  apply (rule eq_reflection)
+lemma sum_map_id[id_simps]:
+  shows "sum_map id id = id"
   apply (rule ext)
   apply (case_tac x)
   apply (auto)
   done
 
-lemma sum_rel_eq[id_simps]: 
-  "sum_rel op = op = \<equiv> op ="
-  apply (rule eq_reflection)
+lemma sum_rel_eq[id_simps]:
+  "(sum_rel op = op =) = op ="
   apply (rule ext)+
   apply (case_tac x)
   apply auto