Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Nominal2_FSet.thy
changeset 1675 d24f59f78a86
parent 1568 2311a9fc4624
child 1682 ae54ce4cde54 
--- a/Nominal/Nominal2_FSet.thy	Sat Mar 27 09:15:09 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Sat Mar 27 09:21:43 2010 +0100
@@ -44,7 +44,7 @@
 
 end
 
-lemma permute_fset[simp,eqvt]:
+lemma permute_fset[eqvt]:
   "p \<bullet> ({||} :: 'a :: pt fset) = {||}"
   "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
   by (lifting permute_list.simps)
nominal2