# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271581109 -7200
# Node ID 26c0c35641cbf944582273708c2a053a6a129fc0
# Parent  f4477d3fe520849001f1b0968714afba61fcf2b4
equivariance for alpha_raw in CoreHaskell is automatically derived

diff -r f4477d3fe520 -r 26c0c35641cb Nominal/Ex/ExCoreHaskell.thy
--- a/Nominal/Ex/ExCoreHaskell.thy	Sun Apr 18 09:26:38 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Sun Apr 18 10:58:29 2010 +0200
@@ -679,5 +679,18 @@
   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 qed
 
+section {* test about equivariance for alpha *}
+
+thm eqvts
+thm eqvts_raw
+
+declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_tkind_raw
+
+thm eqvts
+thm eqvts_raw
+
 end