# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267538750 -3600
# Node ID e965524c3301f6c66b491952d674a57082342f46
# Parent  61319a9af976687f7ae2ac6c4178ae7eb428eb76
added distinctness of perms

diff -r 61319a9af976 -r e965524c3301 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Tue Mar 02 15:05:35 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 02 15:05:50 2010 +0100
@@ -351,8 +351,6 @@
 notation 
   alpha1 ("_ \<approx>abs1 _")
 
-thm swap_set_not_in
-
 lemma qq:
   fixes S::"atom set"
   assumes a: "supp p \<inter> S = {}"
@@ -502,6 +500,15 @@
 apply(simp)
 oops
 
+fun
+  distinct_perms 
+where
+  "distinct_perms [] = True"
+| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
+
+
+
+
 
 end