1 theory ExLet

     2 imports "Parser"

     3 begin

     4 

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

     6 

     7 atom_decl name

     8 

     9 ML {* val _ = recursive := false  *}

    10 nominal_datatype trm =

    11   Vr "name"

    12 | Ap "trm" "trm"

    13 | Lm x::"name" t::"trm"  bind x in t

    14 | Lt a::"lts" t::"trm"   bind "bv a" in t

    15 and lts =

    16   Nil

    17 | Cons "name" "trm" "lts"

    18 binder

    19   bn

    20 where

    21   "bn Nil = {}"

    22 | "bn (Cons x t l) = {atom x} \<union> (bn l)"

    23 

    24 thm trm_lts.fv

    25 thm trm_lts.eq_iff

    26 thm trm_lts.bn

    27 thm trm_lts.perm

    28 thm trm_lts.induct

    29 thm trm_lts.distinct

    30 thm trm_lts.fv[simplified trm_lts.supp]

    31 

    32 end

    33 

    34 

    35