Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generalised the supp for atoms to all concrete atoms (not just names)
authorChristian Urban <urbanc@in.tum.de>
Thu, 11 Mar 2010 19:43:50 +0100
changeset 1432 b41de1879dae
parent 1431 bc9ed52bcef5
child 1433 7a9217a7f681
generalised the supp for atoms to all concrete atoms (not just names)
Nominal/Abs.thy file | annotate | diff | comparison | revisions 
--- 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)
nominal2