changeset 1739 | 468c3c1adcba |
parent 1731 | 3832a31a73b1 |
child 1757 | d803c0adfcf8 |
--- a/Nominal/ExLet.thy Thu Apr 01 01:05:05 2010 +0200 +++ b/Nominal/ExLet.thy Thu Apr 01 03:28:28 2010 +0200 @@ -6,7 +6,7 @@ atom_decl name -ML {* val _ = recursive := false *} +ML {* val _ = recursive := true *} ML {* val _ = alpha_type := AlphaLst *} nominal_datatype trm = Vr "name" @@ -36,6 +36,7 @@ (*thm trm_lts.supp*) thm trm_lts.fv[simplified trm_lts.supp(1-2)] + primrec permute_bn_raw where