# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273499104 -7200
# Node ID 751d1349329b35050ca99bc455c8b253aa1d1ea4
# Parent  c0ab7451b20dd1f697a439680aaf1d509be0189c# Parent  1f38489f1cf0f7ed0ef3f737b8d67589ea25daa0
merge

diff -r 1f38489f1cf0 -r 751d1349329b Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon May 10 15:14:02 2010 +0200
+++ b/Nominal/Abs.thy	Mon May 10 15:45:04 2010 +0200
@@ -840,5 +840,14 @@
   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
+lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
+  by auto
+
+lemma [eqvt]: "(p \<bullet> prod_rel A B x y) = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+  by (simp, perm_simp) (rule refl)
+
+lemma [eqvt]: "(p \<bullet> prod_fv A B (x, y)) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+  by (simp, perm_simp) (rule refl)
+
 end