changeset 42156 | df219e736a5d |
parent 42051 | dbdd4790da34 |
child 42284 | 326f57825e1a |
--- a/src/CCL/Term.thy Tue Mar 29 23:15:25 2011 +0200 +++ b/src/CCL/Term.thy Tue Mar 29 23:27:38 2011 +0200 @@ -111,8 +111,7 @@ consts napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) -axioms - +defs one_def: "one == true" if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" inl_def: "inl(a) == <true,a>"