1 theory ExLet

     1 theory ExLet

     3 begin

     3 begin

     4 

     4 

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

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

     6 

     6 

     7 atom_decl name

     7 atom_decl name

     8 

     8 

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

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

    11 

    10 

    12 nominal_datatype trm =

    11 nominal_datatype trm =

    13   Vr "name"

    12   Vr "name"

    14 | Ap "trm" "trm"

    13 | Ap "trm" "trm"

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

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

    20 binder

    19 binder

    21   bn

    20   bn

    22 where

    21 where

    23   "bn Lnil = {}"

    22   "bn Lnil = {}"

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

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

    25 

    26 

    26 thm trm_lts.fv

    27 thm trm_lts.fv

    27 thm trm_lts.eq_iff

    28 thm trm_lts.eq_iff

    28 thm trm_lts.bn

    29 thm trm_lts.bn

    29 thm trm_lts.perm

    30 thm trm_lts.perm