# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273509170 -7200
# Node ID f81e0f9f2b2eb9eefebe25743f9fe3836d453ea1
# Parent  41c2445fdee4614c0cf52f85a98470defa13b620# Parent  60ce41a111808a653c8194090eac616557c873c2
merge

diff -r 60ce41a11180 -r f81e0f9f2b2e Nominal/Ex/Ex1rec.thy
--- a/Nominal/Ex/Ex1rec.thy	Mon May 10 18:32:15 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy	Mon May 10 18:32:50 2010 +0200
@@ -5,6 +5,7 @@
 atom_decl name
 
 ML {* val _ = cheat_supp_eq := true *}
+ML {* val _ = cheat_equivp := true *}
 
 nominal_datatype lam =
   Var "name"
diff -r 60ce41a11180 -r f81e0f9f2b2e Nominal/Ex/ExLetRec.thy
--- a/Nominal/Ex/ExLetRec.thy	Mon May 10 18:32:15 2010 +0200
+++ b/Nominal/Ex/ExLetRec.thy	Mon May 10 18:32:50 2010 +0200
@@ -7,7 +7,6 @@
 
 atom_decl name
 
-ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = cheat_equivp := true *}
 
 nominal_datatype trm =
@@ -83,12 +82,6 @@
   apply (simp add: atom_eqvt fresh_star_def)
   done
 
-(*
-declare permute_trm_raw_permute_lts_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
-equivariance alpha_trm_raw
-*)
-
 end