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/Ex/Lambda.thy
changeset 2982 4a00077c008f
parent 2975 c62e26830420
child 2995 6d2859aeebba 
--- a/Nominal/Ex/Lambda.thy	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Fri Jul 22 11:37:16 2011 +0100
@@ -644,8 +644,8 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Inl var_fresh_subst)
   apply(simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
 done
nominal2