--- a/Nominal/Ex/LamTest.thy	Sun Jan 09 05:38:53 2011 +0000
+++ b/Nominal/Ex/LamTest.thy	Mon Jan 10 08:51:51 2011 +0000
@@ -12,6 +12,20 @@
 definition
  "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
 
+lemma supp_eqvt_at:
+  assumes asm: "eqvt_at f x"
+  and     fin: "finite (supp x)"
+  shows "supp (f x) \<subseteq> supp x"
+apply(rule supp_is_subset)
+unfolding supports_def
+unfolding fresh_def[symmetric]
+using asm
+apply(simp add: eqvt_at_def)
+apply(simp add: swap_fresh_fresh)
+apply(rule fin)
+done
+
+
 definition
  "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
 
@@ -500,6 +514,7 @@
 *}
 
 ML Thm.forall_elim_vars
+ML Thm.implies_intr
 
 ML {* (ex1_implies_ex, ex1_implies_un) *}
 thm fundef_ex1_eqvt_at