diff -r f5aa2134e199 -r 670701b19e8e Nominal/Abs.thy --- a/Nominal/Abs.thy Tue Mar 02 21:43:27 2010 +0100 +++ b/Nominal/Abs.thy Wed Mar 03 11:50:25 2010 +0100 @@ -415,9 +415,10 @@ apply(simp add: supp_swap) done -(* + thm supp_perm +(* lemma perm_induct_test: fixes P :: "perm => bool" assumes zero: "P 0"