--- a/src/HOL/Nominal/Nominal.thy Mon Nov 13 11:41:40 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy Mon Nov 13 12:10:49 2006 +0100
@@ -344,6 +344,16 @@
lemma fresh_prod_elim: "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
by rule (simp_all add: fresh_prod)
+lemma fresh_prodD:
+ "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> x"
+ "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y"
+ by (simp_all add: fresh_prod)
+
+ML_setup {*
+ val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD") :: mksimps_pairs;
+ change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
+*}
+
section {* Abstract Properties for Permutations and Atoms *}
(*=========================================================*)