diff -r e125fc7a1183 -r 5750eba8820d src/CCL/Hered.thy --- a/src/CCL/Hered.thy Wed Jun 21 11:35:10 1995 +0200 +++ b/src/CCL/Hered.thy Wed Jun 21 15:01:07 1995 +0200 @@ -23,8 +23,8 @@ (*** Definitions of Hereditary Termination ***) HTTgen_def - "HTTgen(R) == {t. t=true | t=false | (EX a b.t= & a : R & b : R) | \ -\ (EX f. t=lam x.f(x) & (ALL x.f(x) : R))}" + "HTTgen(R) == {t. t=true | t=false | (EX a b.t= & a : R & b : R) | + (EX f. t=lam x.f(x) & (ALL x.f(x) : R))}" HTT_def "HTT == gfp(HTTgen)" end