# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285575036 14400
# Node ID c0695bb33fcd44ed2a58061d7f55d4c020f38978
# Parent  fbdaaa20396b993abf441453f31ff9d69fb9981b
added simp rules for prod_fv and prod_alpha

diff -r fbdaaa20396b -r c0695bb33fcd Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Sep 25 08:38:04 2010 -0400
+++ b/Nominal/Abs.thy	Mon Sep 27 04:10:36 2010 -0400
@@ -570,6 +570,16 @@
   unfolding prod_fv.simps
   by (perm_simp) (rule refl)
 
+lemma prod_fv_supp:
+  shows "prod_fv supp supp = supp"
+by (rule ext)
+   (auto simp add: prod_fv.simps supp_Pair)
+
+lemma prod_alpha_eq:
+  shows "prod_alpha (op=) (op=) = (op=)"
+unfolding prod_alpha_def
+by (auto intro!: ext)
+
 
 end