# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267546318 -3600
# Node ID 43d6e37303533f466215a28aa156670c8b2f33c4
# Parent  6d851952799c14b245ed79bcddacb314f3a7161c
Add image_eqvt and atom_eqvt to eqvt bases.

diff -r 6d851952799c -r 43d6e3730353 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Tue Mar 02 17:11:19 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Tue Mar 02 17:11:58 2010 +0100
@@ -5,7 +5,7 @@
     (Contains most, but not all such lemmas.)
 *)
 theory Nominal2_Eqvt
-imports Nominal2_Base
+imports Nominal2_Base Nominal2_Atoms
 uses ("nominal_thmdecls.ML")
      ("nominal_permeq.ML")
 begin
@@ -248,7 +248,9 @@
 
   (* sets *)
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
-  Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt
+  Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
+
+  atom_eqvt
 
 thm eqvts
 thm eqvts_raw
@@ -301,4 +303,4 @@
 oops
 
 
-end
\ No newline at end of file
+end