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.
RSP of perms can be shown in one go.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 26 Feb 2010 15:42:00 +0100
changeset 1279 d53b7f24450b
parent 1278 8814494fe4da
child 1280 1f057f8da8aa
RSP of perms can be shown in one go.
Nominal/LFex.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/LFex.thy	Fri Feb 26 15:10:55 2010 +0100
+++ b/Nominal/LFex.thy	Fri Feb 26 15:42:00 2010 +0100
@@ -93,11 +93,7 @@
 
 local_setup {* snd o prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]
   (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]
-  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]
-  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]
+local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}, @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}, @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
   @{thms rfv_rsp} @{thms alpha_equivps} 1 *}
nominal2