# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264486450 -3600
# Node ID c445b6aeefc9c7902cb8e83891f35348c588f2be
# Parent  8d51795ef54df6f301029d70f9cf20b279b62436
Removing more eq_reflections.

diff -r 8d51795ef54d -r c445b6aeefc9 Quot/QuotBase.thy
--- a/Quot/QuotBase.thy	Mon Jan 25 20:47:20 2010 +0100
+++ b/Quot/QuotBase.thy	Tue Jan 26 07:14:10 2010 +0100
@@ -72,8 +72,7 @@
 where
   "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
 
-lemma eq_comp_r: "op = OO R OO op = \<equiv> R"
-  apply (rule eq_reflection)
+lemma eq_comp_r: "(op = OO R OO op =) = R"
   apply (rule ext)+
   apply auto
   done
@@ -108,8 +107,8 @@
   by (simp add: expand_fun_eq id_def)
 
 lemma fun_rel_eq:
-  shows "(op =) ===> (op =) \<equiv> (op =)"
-  by (rule eq_reflection) (simp add: expand_fun_eq)
+  shows "((op =) ===> (op =)) = (op =)"
+  by (simp add: expand_fun_eq)
 
 lemma fun_rel_id:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"