--- a/src/CCL/Fix.thy Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Fix.thy Fri Oct 10 17:10:12 1997 +0200
@@ -17,10 +17,10 @@
rules
idgen_def
- "idgen(f) == lam t.case(t,true,false,%x y.<f`x, f`y>,%u.lam x.f ` u(x))"
+ "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)))"
end