src/CCL/Term.thy
 changeset 1149 5750eba8820d parent 998 91d09e262799 child 1474 3f7d67927fe2
```--- a/src/CCL/Term.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/CCL/Term.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -75,13 +75,13 @@
letrec_def
"letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"

-  letrec2_def  "letrec g x y be h(x,y,g) in f(g)== \
-\               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) \
-\                          in f(%x y.g'(<x,y>))"
+  letrec2_def  "letrec g x y be h(x,y,g) in f(g)==
+               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>)))
+                          in f(%x y.g'(<x,y>))"

-  letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == \
-\             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) \
-\                          in f(%x y z.g'(<x,<y,z>>))"
+  letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) ==
+             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>))))
+                          in f(%x y z.g'(<x,<y,z>>))"

napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
```