changeset 1432 | b41de1879dae |
parent 1431 | bc9ed52bcef5 |
child 1433 | 7a9217a7f681 |
--- a/Nominal/Abs.thy Thu Mar 11 19:41:11 2010 +0100 +++ b/Nominal/Abs.thy Thu Mar 11 19:43:50 2010 +0100 @@ -725,8 +725,6 @@ (* support of concrete atom sets *) -atom_decl name - lemma atom_eqvt_raw: fixes p::"perm" shows "(p \<bullet> atom) = atom" @@ -739,7 +737,7 @@ done lemma - fixes as::"name set" + fixes as::"'a::at_base set" shows "supp (atom ` as) = supp as" apply(simp add: supp_def) apply(simp add: image_eqvt)