--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CCL/Fix.thy Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,26 @@
+(* Title: CCL/Lazy/fix.thy
+ ID: $Id$
+ Author: Martin Coen
+ Copyright 1993 University of Cambridge
+
+Tentative attempt at including fixed point induction.
+Justified by Smith.
+*)
+
+Fix = Type +
+
+consts
+
+ idgen :: "[i]=>i"
+ INCL :: "[i=>o]=>o"
+
+rules
+
+ 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)))"
+
+end