theory ExLet
imports "Parser"
begin

text {* example 3 or example 5 from Terms.thy *}

atom_decl name

ML {* val _ = recursive := false  *}
nominal_datatype trm =
  Vr "name"
| Ap "trm" "trm"
| Lm x::"name" t::"trm"  bind x in t
| Lt a::"lts" t::"trm"   bind "bv a" in t
and lts =
  Nil
| Cons "name" "trm" "lts"
binder
  bn
where
  "bn Nil = {}"
| "bn (Cons x t l) = {atom x} \<union> (bn l)"

thm trm_lts.fv
thm trm_lts.eq_iff
thm trm_lts.bn
thm trm_lts.perm
thm trm_lts.induct
thm trm_lts.distinct
thm trm_lts.fv[simplified trm_lts.supp]

end