Nominal/Ex/Foo1.thy
changeset 2950 0911cb7bf696
parent 2630 8268b277d240
equal deleted inserted replaced
2949:adf22ee09738 2950:0911cb7bf696
    11 atom_decl name
    11 atom_decl name
    12 
    12 
    13 nominal_datatype foo: trm =
    13 nominal_datatype foo: trm =
    14   Var "name"
    14   Var "name"
    15 | App "trm" "trm"
    15 | App "trm" "trm"
    16 | Lam x::"name" t::"trm"  bind x in t
    16 | Lam x::"name" t::"trm"    binds x in t
    17 | Let1 a::"assg" t::"trm"  bind "bn1 a" in t
    17 | Let1 a::"assg" t::"trm"   binds "bn1 a" in t
    18 | Let2 a::"assg" t::"trm"  bind "bn2 a" in t
    18 | Let2 a::"assg" t::"trm"   binds "bn2 a" in t
    19 | Let3 a::"assg" t::"trm"  bind "bn3 a" in t
    19 | Let3 a::"assg" t::"trm"   binds "bn3 a" in t
    20 | Let4 a::"assg'" t::"trm"  bind (set) "bn4 a" in t
    20 | Let4 a::"assg'" t::"trm"  binds (set) "bn4 a" in t
    21 and assg =
    21 and assg =
    22   As "name" "name" "trm"
    22   As "name" "name" "trm"
    23 and assg' =
    23 and assg' =
    24   BNil
    24   BNil
    25 | BAs "name" "assg'"
    25 | BAs "name" "assg'"