Nominal/Ex/LetPat.thy
changeset 2950 0911cb7bf696
parent 2648 5d9724ad543d
child 3029 6fd3fc3254ee
equal deleted inserted replaced
2949:adf22ee09738 2950:0911cb7bf696
     5 atom_decl name
     5 atom_decl name
     6 
     6 
     7 nominal_datatype trm =
     7 nominal_datatype trm =
     8   Var "name"
     8   Var "name"
     9 | App "trm" "trm"
     9 | App "trm" "trm"
    10 | Lam x::"name" t::"trm"       bind (set) x in t
    10 | Lam x::"name" t::"trm"       binds (set) x in t
    11 | Let p::"pat" "trm" t::"trm"  bind (set) "f p" in t
    11 | Let p::"pat" "trm" t::"trm"  binds (set) "f p" in t
    12 and pat =
    12 and pat =
    13   PN
    13   PN
    14 | PS "name"
    14 | PS "name"
    15 | PD "name" "name"
    15 | PD "name" "name"
    16 binder
    16 binder