--- a/src/CCL/Fix.thy Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/Fix.thy Sat Sep 17 17:35:26 2005 +0200
@@ -1,26 +1,27 @@
-(* Title: CCL/Lazy/fix.thy
+(* Title: CCL/Fix.thy
ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
-
-Tentative attempt at including fixed point induction.
-Justified by Smith.
*)
-Fix = Type +
+header {* Tentative attempt at including fixed point induction; justified by Smith *}
+
+theory Fix
+imports Type
+begin
consts
-
idgen :: "[i]=>i"
INCL :: "[i=>o]=>o"
-rules
-
- idgen_def
+axioms
+ idgen_def:
"idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
- 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)))"
+ 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)))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end