src/CCL/Term.thy
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>"