1 theory ExLetMult

     2 imports "../NewParser"

     3 begin

     4 

     5 atom_decl name

     6 

     7 nominal_datatype trm =

     8   Vr "name"

     9 | Ap "trm" "trm"

    10 | Lm x::"name" t::"trm" bind_set x in t

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

    12 and lts =

    13   Lnil

    14 | Lcons "name" "trm" "lts"

    15 binder

    16   bn

    17 where

    18   "bn Lnil = []"

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

    20 

    21 thm trm_lts.eq_iff

    22 thm trm_lts.induct

    23 thm trm_lts.fv[simplified trm_lts.supp]

    24 

    25 

    26 

    27 end

    28 

    29 

    30