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 1001 9e3c8de7a61c
parent 997 b7d259ded92e
child 1009 2ebfbd861846 
--- a/Quot/Nominal/LamEx.thy	Mon Feb 01 10:00:03 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 01 11:00:51 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