# HG changeset patch
# User wenzelm
# Date 1163416249 -3600
# Node ID edb595802d22e8f896db5e63ca38fa29e2daf479
# Parent  ebd2704ed33ba13ccec0a888249431d483734d5e
added fresh_prodD, which is included fresh_prodD into mksimps setup;

diff -r ebd2704ed33b -r edb595802d22 src/HOL/Nominal/Nominal.thy
--- 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 *}
 (*=========================================================*)