Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 03 Feb 2010 13:00:37 +0100
changeset 1047 0f101870e2ff
parent 1046 159c7a9cd575 (current diff)
parent 1045 7a975641efbc (diff)
child 1049 a83ee7ecb1cb
child 1050 e8bb5f85e510
merge
--- a/Quot/Nominal/LFex.thy	Wed Feb 03 13:00:07 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 03 13:00:37 2010 +0100
@@ -652,15 +652,15 @@
 apply(simp add: KIND_TY_TRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
-apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
+apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
 apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")
 apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
 apply(simp add: KIND_TY_TRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
 apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")
 apply(simp add: supp_Abs Set.Un_commute)
@@ -668,7 +668,7 @@
 apply(simp add: KIND_TY_TRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
 done
nominal2