1 theory LetRec2

     1 theory LetRec2

     2 imports "../Nominal2"

     2 imports "../Nominal2"

     3 begin

     3 begin

     4 

     4 

     5 atom_decl name

     5 atom_decl name

     7 

     6 

     8 nominal_datatype trm =

     7 nominal_datatype trm =

     9   Vr "name"

     8   Vr "name"

    10 | Ap "trm" "trm"

     9 | Ap "trm" "trm"

    11 | Lm x::"name" t::"trm"  bind (set) x in t

    10 | Lm x::"name" t::"trm"  bind (set) x in t

    24 thm trm_lts.eq_iff

    23 thm trm_lts.eq_iff

    25 thm trm_lts.bn_defs

    24 thm trm_lts.bn_defs

    26 thm trm_lts.perm_simps

    25 thm trm_lts.perm_simps

    27 thm trm_lts.induct

    26 thm trm_lts.induct

    28 thm trm_lts.distinct

    27 thm trm_lts.distinct

    29 

    32 

    30 

    33 

    31 (* why is this not in HOL simpset? *)

    34 (* why is this not in HOL simpset? *)

    32 (*

    35 (*

    33 lemma set_sub: "{a, b} - {b} = {a} - {b}"

    36 lemma set_sub: "{a, b} - {b} = {a} - {b}"