Nominal/ExLet.thy
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