changeset 3089 | 9bcf02a6eea9 |
parent 2998 | f0fab367453a |
child 3186 | 425b4c406d80 |
--- a/Nominal/Ex/CPS/Lt.thy Wed Dec 21 15:47:42 2011 +0900 +++ b/Nominal/Ex/CPS/Lt.thy Wed Dec 21 17:05:00 2011 +0900 @@ -7,8 +7,8 @@ nominal_datatype lt = Var name ("_~" [150] 149) + | App lt lt (infixl "$" 100) | Lam x::"name" t::"lt" binds x in t - | App lt lt (infixl "$" 100) nominal_primrec subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90)