# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272888210 -7200
# Node ID d974059827adf8cc2a079f9da086101b5a84ad01
# Parent  e32ec6e61154424d19a295c7604fd522805a26fe
Equivariance fails for single let?

diff -r e32ec6e61154 -r d974059827ad Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon May 03 13:42:44 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Mon May 03 14:03:30 2010 +0200
@@ -1,16 +1,16 @@
 theory SingleLet
-imports "../Parser"
+imports "../NewParser"
 begin
 
 atom_decl name
 
-ML {* val _ = recursive := false *}
+ML {* val _ = cheat_alpha_eqvt := true *}
 
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
-| Let a::"assg" t::"trm"  bind "bn a" in t
+| Lam x::"name" t::"trm"  bind_set x in t
+| Let a::"assg" t::"trm"  bind_set "bn a" in t
 and assg =
   As "name" "trm"
 binder
@@ -18,19 +18,23 @@
 where
   "bn (As x t) = {atom x}"
 
-print_theorems
 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
-
 thm trm_assg.fv
 thm trm_assg.supp
-thm trm_assg.eq_iff[simplified alphas_abs[symmetric]]
+thm trm_assg.eq_iff
 thm trm_assg.bn
 thm trm_assg.perm
 thm trm_assg.induct
 thm trm_assg.inducts
 thm trm_assg.distinct
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
-thm trm_assg.fv[simplified trm_assg.supp]
+thm trm_assg.fv[simplified trm_assg.supp(1-2)]
+
+setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+declare permute_trm_raw_permute_assg_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_trm_raw
+
 
 end