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 2542 1f5c8e85c41f
parent 2540 135ac0fb2686
child 2550 551c5a8b6b2c 
--- a/Nominal/Nominal2_FSet.thy	Sun Oct 17 15:28:05 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Sun Oct 17 15:53:37 2010 +0100
@@ -72,7 +72,7 @@
 
 lemma atom_map_fset_cong:
   shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"
-  apply(rule inj_map_fset_eq_iff)
+  apply(rule inj_map_fset_cong)
   apply(simp add: inj_on_def)
   done
nominal2