# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259911196 -3600
# Node ID d62b6517a0ab82619fd70c24827f9bda64f89002
# Parent  fac6069d8e80215ebc2d4eab0c63a1eb9d605af4# Parent  f7569f994195690747801e89e2546f1f96b6f6bf
merge

diff -r fac6069d8e80 -r d62b6517a0ab FSet.thy
diff -r fac6069d8e80 -r d62b6517a0ab QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 08:18:38 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 08:19:56 2009 +0100
@@ -741,6 +741,7 @@
      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
 *}
 
+
 lemma FUN_REL_I:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   shows "(R1 ===> R2) f g"