changeset 2950 | 0911cb7bf696 |
parent 2648 | 5d9724ad543d |
child 3029 | 6fd3fc3254ee |
--- a/Nominal/Ex/LetPat.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetPat.thy Tue Jul 05 18:42:34 2011 +0200 @@ -7,8 +7,8 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind (set) x in t -| Let p::"pat" "trm" t::"trm" bind (set) "f p" in t +| Lam x::"name" t::"trm" binds (set) x in t +| Let p::"pat" "trm" t::"trm" binds (set) "f p" in t and pat = PN | PS "name"