# HG changeset patch # User Christian Urban # 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 ("_ \abs1 _") -thm swap_set_not_in - lemma qq: fixes S::"atom set" assumes a: "supp p \ S = {}" @@ -502,6 +500,15 @@ apply(simp) oops +fun + distinct_perms +where + "distinct_perms [] = True" +| "distinct_perms (p # ps) = (supp p \ supp ps = {} \ distinct_perms ps)" + + + + end