changeset 2950 | 0911cb7bf696 |
parent 2616 | dd7490fdd998 |
child 3029 | 6fd3fc3254ee |
--- a/Nominal/Ex/LetFun.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/LetFun.thy Tue Jul 05 18:42:34 2011 +0200 @@ -12,7 +12,7 @@ nominal_datatype exp = Var name | Pair exp exp -| LetRec x::name p::pat e1::exp e2::exp bind x in e2, bind x "bp p" in e1 +| LetRec x::name p::pat e1::exp e2::exp binds x in e2, binds x "bp p" in e1 and pat = PVar name | PUnit