Nominal/Ex/Let_ExhaustIssue.thy
changeset 2950 0911cb7bf696
parent 2930 1d9e50934bc5
child 3235 5ebd327ffb96
equal deleted inserted replaced
2949:adf22ee09738 2950:0911cb7bf696
     6 atom_decl name
     6 atom_decl name
     7 
     7 
     8 nominal_datatype trm =
     8 nominal_datatype trm =
     9   Var "name"
     9   Var "name"
    10 | App "trm" "trm"
    10 | App "trm" "trm"
    11 | Lam x::"name" t::"trm"  bind  x in t
    11 | Lam x::"name" t::"trm"  binds  x in t
    12 | Let as::"assn" t::"trm"   bind "bn as" in t
    12 | Let as::"assn" t::"trm"   binds "bn as" in t
    13 and assn =
    13 and assn =
    14   ANil
    14   ANil
    15 | ACons "name" "trm" "assn"
    15 | ACons "name" "trm" "assn"
    16 binder
    16 binder
    17   bn
    17   bn