src/CCL/Hered.thy
changeset 3837 d7f033c74b38
parent 1474 3f7d67927fe2
child 17456 bcf7544875b2
equal deleted inserted replaced
3836:f1a1817659e6 3837:d7f033c74b38
    21 rules
    21 rules
    22 
    22 
    23   (*** Definitions of Hereditary Termination ***)
    23   (*** Definitions of Hereditary Termination ***)
    24 
    24 
    25   HTTgen_def 
    25   HTTgen_def 
    26   "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | 
    26   "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b>      & a : R & b : R) | 
    27                                       (EX f.  t=lam x.f(x) & (ALL x.f(x) : R))}"
    27                                       (EX f.  t=lam x. f(x) & (ALL x. f(x) : R))}"
    28   HTT_def       "HTT == gfp(HTTgen)"
    28   HTT_def       "HTT == gfp(HTTgen)"
    29 
    29 
    30 end
    30 end