# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267195320 -3600
# Node ID d53b7f24450b26bcc8e84a3a0daf0a6c7f35d020
# Parent  8814494fe4da14606ae256e1958d12082a07e28d
RSP of perms can be shown in one go.

diff -r 8814494fe4da -r d53b7f24450b Nominal/LFex.thy
--- 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 *}