src/CCL/Term.thy
changeset 1149 5750eba8820d
parent 998 91d09e262799
child 1474 3f7d67927fe2
     1.1 --- a/src/CCL/Term.thy	Wed Jun 21 11:35:10 1995 +0200
     1.2 +++ b/src/CCL/Term.thy	Wed Jun 21 15:01:07 1995 +0200
     1.3 @@ -75,13 +75,13 @@
     1.4    letrec_def    
     1.5    "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
     1.6  
     1.7 -  letrec2_def  "letrec g x y be h(x,y,g) in f(g)== \
     1.8 -\               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) \
     1.9 -\                          in f(%x y.g'(<x,y>))"
    1.10 +  letrec2_def  "letrec g x y be h(x,y,g) in f(g)== 
    1.11 +               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) 
    1.12 +                          in f(%x y.g'(<x,y>))"
    1.13  
    1.14 -  letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == \
    1.15 -\             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) \
    1.16 -\                          in f(%x y z.g'(<x,<y,z>>))"
    1.17 +  letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == 
    1.18 +             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) 
    1.19 +                          in f(%x y z.g'(<x,<y,z>>))"
    1.20  
    1.21    napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
    1.22