# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322299459 0
# Node ID 7519ebb4114590961aa7b02a4a2f2c528b54384e
# Parent  83744806b6604ad8b568bc08d262712fe849c9d2
added eqvt-lemma for Image

diff -r 83744806b660 -r 7519ebb41145 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu Nov 10 01:15:19 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Sat Nov 26 09:24:19 2011 +0000
@@ -906,6 +906,11 @@
   unfolding image_def
   by (perm_simp) (rule refl)
 
+lemma Image_eqvt [eqvt]:
+  shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)"
+  unfolding Image_def
+  by (perm_simp) (rule refl)
+
 lemma UNIV_eqvt [eqvt]:
   shows "p \<bullet> UNIV = UNIV"
   unfolding UNIV_def