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.
Quot/Nominal/LamEx.thy
changeset 997 b7d259ded92e
parent 995 ee0619b5adff
child 1009 2ebfbd861846 
--- a/Quot/Nominal/LamEx.thy	Sat Jan 30 12:12:52 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 01 09:56:32 2010 +0100
@@ -548,7 +548,7 @@
 
 lemma app_supp:
   shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"
-apply(simp only: permute_lam supp_def lam_inject)
+apply(simp only: supp_def lam_inject)
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done
nominal2