src/CCL/Fix.thy

--- a/src/CCL/Fix.thy	Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/Fix.thy	Wed Oct 03 21:29:05 2007 +0200
@@ -14,10 +14,11 @@
   idgen      ::       "[i]=>i"
   INCL      :: "[i=>o]=>o"
 
-axioms
+defs
   idgen_def:
   "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
 
+axioms
   INCL_def:   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
   po_INCL:    "INCL(%x. a(x) [= b(x))"
   INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"