changeset 2950 | 0911cb7bf696 |
parent 2877 | 3e82c1ced5e4 |
child 2971 | d629240f0f63 |
--- a/Nominal/Ex/LetRec.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetRec.thy Tue Jul 05 18:42:34 2011 +0200 @@ -8,8 +8,8 @@ trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind (set) x in t -| Let_Rec bp::"bp" t::"trm" bind (set) "bn bp" in bp t +| Lam x::"name" t::"trm" binds (set) x in t +| Let_Rec bp::"bp" t::"trm" binds (set) "bn bp" in bp t and bp = Bp "name" "trm" binder