# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1309198435 -3600
# Node ID ad426ba606063d6060e45dbd52e9179a555c3a7e
# Parent  9096338a79858fe7e2e990850fbaaa8b960bf02f
renamed ds to dset (disagreement set)

diff -r 9096338a7985 -r ad426ba60606 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jun 27 12:15:21 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon Jun 27 19:13:55 2011 +0100
@@ -2273,7 +2273,6 @@
   qed
 qed
 
-
 lemma supp_perm_perm_eq:
   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"
   shows "p \<bullet> x = q \<bullet> x"
@@ -2291,18 +2290,17 @@
 text {* disagreement set *}
 
 definition
-  ds :: "perm \<Rightarrow> perm \<Rightarrow> atom set"
+  dset :: "perm \<Rightarrow> perm \<Rightarrow> atom set"
 where
-  "ds p q = {a::atom. p \<bullet> a \<noteq> q \<bullet> a}"
+  "dset p q = {a::atom. p \<bullet> a \<noteq> q \<bullet> a}"
 
 lemma ds_fresh:
-  assumes "ds p q \<sharp>* x"
+  assumes "dset p q \<sharp>* x"
   shows "p \<bullet> x = q \<bullet> x"
 using assms
-unfolding ds_def fresh_star_def fresh_def
+unfolding dset_def fresh_star_def fresh_def
 by (auto intro: supp_perm_perm_eq)
 
-    
 lemma atom_set_perm_eq:
   assumes a: "as \<sharp>* p"
   shows "p \<bullet> as = as"