diff -r 003c7e290a04 -r b0eae8c93314 Nominal/Abs.thy --- a/Nominal/Abs.thy Tue Mar 02 15:07:27 2010 +0100 +++ b/Nominal/Abs.thy Tue Mar 02 16:03:19 2010 +0100 @@ -500,5 +500,14 @@ oops *) + +fun + distinct_perms +where + "distinct_perms [] = True" +| "distinct_perms (p # ps) = (supp p \ supp ps = {} \ distinct_perms ps)" + + + end