12 | App "trm" "trm"

    12 | App "trm" "trm"

    13 | Lam x::"name" t::"trm"  bind_set x in t

    13 | Lam x::"name" t::"trm"  bind_set x in t

    14 | Let a::"assg" t::"trm"  bind_set "bn a" in t

    14 | Let a::"assg" t::"trm"  bind_set "bn a" in t

    15 | Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t

    15 | Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t

    16 | Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t

    16 | Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t

    17 and assg =

    18 and assg =

    18   As "name" "trm"

    19   As "name" "trm"

    19 binder

    20 binder

    20   bn::"assg \<Rightarrow> atom set"

    21   bn::"assg \<Rightarrow> atom set"

    21 where

    22 where

    23 

    24 

    24 thm trm_assg.distinct

    25 thm trm_assg.distinct

    25 thm trm_assg.eq_iff

    26 thm trm_assg.eq_iff

    26 thm trm_assg.supp

    27 thm trm_assg.supp

    27 thm trm_assg.perm

    28 thm trm_assg.perm

    28 

    30 

    29 thm permute_trm_raw_permute_assg_raw.simps

    31 thm permute_trm_raw_permute_assg_raw.simps

    30 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]

    32 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]

    31 

    33 

    32 (* there is something wrong with the free variables *)

    34 (* there is something wrong with the free variables *)