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 1515 76fa21f27f22
parent 1510 be911e869fde
child 1547 57f7af5d7564 
--- a/Nominal/LFex.thy	Thu Mar 18 14:48:27 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 15:13:20 2010 +0100
@@ -46,7 +46,7 @@
   "supp (App M N) = supp M \<union> supp N"
   "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"
   apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt)
-  apply(simp_all only: kind_ty_trm_eq_iff 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)
@@ -57,7 +57,7 @@
 
 lemma supp_fv:
   "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"
-  apply(induct rule: kind_ty_trm_induct)
+  apply(induct rule: kind_ty_trm.induct)
   apply(simp_all (no_asm) only: supp_eqs)
   apply(simp_all)
   apply(simp_all add: supp_eqs)
nominal2