# HG changeset patch # User Cezary Kaliszyk # 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: "\x y. R1 x y \ R2 (f x) (g y)" shows "(R1 ===> R2) f g"