# HG changeset patch # User Cezary Kaliszyk # Date 1273497242 -7200 # Node ID 1f38489f1cf0f7ed0ef3f737b8d67589ea25daa0 # Parent c00885a1534d5c8cf2acd5b363dd0c4b0631ce59 ExLetRec diff -r c00885a1534d -r 1f38489f1cf0 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"