diff -r 1e669b5a75f9 -r 96c627d2815e doc-src/Logics/CTT.tex
--- a/doc-src/Logics/CTT.tex	Thu Nov 11 13:24:47 1993 +0100
+++ b/doc-src/Logics/CTT.tex	Fri Nov 12 10:41:13 1993 +0100
@@ -775,6 +775,7 @@
 {\out Level 0}
 {\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
 {\out  1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\ttbreak
 {\out val prems = ["A type  [A type]",}
 {\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
 {\out              "?x : A ==> C(?x) type  [!!x. x : A ==> C(x) type]",}
@@ -808,6 +809,7 @@
 {\out  1. !!x y xa.}
 {\out        [| x : A; xa : B(x) |] ==>}
 {\out        ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\ttbreak
 {\out  2. !!x y ya.}
 {\out        [| x : A; ya : C(x) |] ==>}
 {\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
@@ -824,6 +826,7 @@
 {\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
 {\out  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
 {\out  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+\ttbreak
 {\out  3. !!x y ya.}
 {\out        [| x : A; ya : C(x) |] ==>}
 {\out        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
@@ -906,6 +909,7 @@
 {\out ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
 {\out  1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
 {\out          (PROD x:A. PROD y:B(x). C(<x,y>))}
+\ttbreak
 {\out val prems = ["A type  [A type]",}
 {\out              "?x : A ==> B(?x) type  [!!x. x : A ==> B(x) type]",}
 {\out              "?z : SUM x:A. B(x) ==> C(?z) type}
@@ -995,9 +999,11 @@
 {\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>}
 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
 {\out  1. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
 {\out        ?b7(uu,x) : B(x)}
+\ttbreak
 {\out  2. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
 {\out        ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)}
@@ -1013,6 +1019,7 @@
 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
 {\out  1. !!uu x. x : A ==> x : A}
 {\out  2. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
@@ -1040,9 +1047,11 @@
 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
 {\out  1. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
 {\out        C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)}
+\ttbreak
 {\out  2. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
 {\out        ?b8(uu,x) : ?A13(uu,x)}
@@ -1055,13 +1064,16 @@
 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
 {\out  1. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
 {\out        (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)}
+\ttbreak
 {\out  2. !!uu x z.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
 {\out           z : ?A14(uu,x) |] ==>}
 {\out        C(x,z) type}
+\ttbreak
 {\out  3. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
 {\out        ?b8(uu,x) : C(x,?c14(uu,x))}
@@ -1074,16 +1086,20 @@
 {\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
 {\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
 {\out   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
 {\out  1. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)}
+\ttbreak
 {\out  2. !!uu x xa.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
 {\out           xa : ?A15(uu,x) |] ==>}
 {\out        fst(uu ` xa) : ?B15(uu,x,xa)}
+\ttbreak
 {\out  3. !!uu x z.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;}
 {\out           z : ?B15(uu,x,x) |] ==>}
 {\out        C(x,z) type}
+\ttbreak
 {\out  4. !!uu x.}
 {\out        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
 {\out        ?b8(uu,x) : C(x,fst(uu ` x))}