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/LFex.thy
changeset 1496 fd483d8f486b
parent 1454 7c8cd6eae8e2
child 1498 2ff84b1f551f 
--- a/Nominal/LFex.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -46,7 +46,7 @@
   "supp (App M N) = supp M \<union> supp N"
   "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
   apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm)
-  apply(simp_all only: kind_ty_trm_inject Abs_eq_iff alpha_gen)
+  apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen)
   apply(simp_all only: ex_out)
   apply(simp_all only: eqvts[symmetric])
   apply(simp_all only: Collect_neg_conj)
nominal2