src/CCL/Fix.thy
changeset 42156 df219e736a5d
parent 36319 8feb2c4bef1a
child 58889 5b7a9633cfa8
--- a/src/CCL/Fix.thy	Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Fix.thy	Tue Mar 29 23:27:38 2011 +0200
@@ -9,17 +9,12 @@
 imports Type
 begin
 
-consts
-  idgen      ::       "[i]=>i"
-  INCL      :: "[i=>o]=>o"
+definition idgen :: "i => i"
+  where "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
 
-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))"
+axiomatization INCL :: "[i=>o]=>o" where
+  INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" and
+  po_INCL: "INCL(%x. a(x) [= b(x))" and
   INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"