ExLetRec
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 10 May 2010 15:14:02 +0200
changeset 2091 1f38489f1cf0
parent 2090 c00885a1534d
child 2093 751d1349329b
ExLetRec
Nominal/Ex/ExLetRec.thy
--- a/Nominal/Ex/ExLetRec.thy	Mon May 10 15:11:19 2010 +0200
+++ b/Nominal/Ex/ExLetRec.thy	Mon May 10 15:14:02 2010 +0200
@@ -7,6 +7,9 @@
 
 atom_decl name
 
+ML {* val _ = cheat_alpha_eqvt := true *}
+ML {* val _ = cheat_equivp := true *}
+
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"