1 theory ExLetMult

     2 imports "Parser"

     3 begin

     4 

     5 atom_decl name

     6 

     7 ML {* val _ = recursive := true *}

     8 ML {* val _ = alpha_type := AlphaLst *}

     9 ML {* val _ = cheat_equivp := true *}

    10 nominal_datatype trm =

    11   Vr "name"

    12 | Ap "trm" "trm"

    13 | Lm "trm" "trm"

    14 | Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t, bind "bn l" in s

    15 and lts =

    16   Lnil

    17 | Lcons "name" "trm" "lts"

    18 binder

    19   bn

    20 where

    21   "bn Lnil = []"

    22 | "bn (Lcons x t l) = (atom x) # (bn l)"

    23 

    24 thm trm_lts.eq_iff

    25 thm trm_lts.induct

    26 thm trm_lts.fv[simplified trm_lts.supp]

    27 

    28 end

    29 

    30 

    31