diff -r a931f1b45151 -r 1b3cddf41b2d doc-src/Logics/LK.tex
--- a/doc-src/Logics/LK.tex	Thu Nov 11 12:44:43 1993 +0100
+++ b/doc-src/Logics/LK.tex	Thu Nov 11 13:18:49 1993 +0100
@@ -40,7 +40,7 @@
 This technique lets Isabelle formalize sequent calculus rules,
 where the comma is the associative operator:
 \[ \infer[\conj\hbox{-left}]
-	 {\Gamma,P\conj Q,\Delta \turn \Theta}
+         {\Gamma,P\conj Q,\Delta \turn \Theta}
          {\Gamma,P,Q,\Delta \turn \Theta}  \] 
 Multiple unifiers occur whenever this is resolved against a goal containing
 more than one conjunction on the left.  Explicit formalization of sequents
@@ -56,25 +56,25 @@
 \begin{figure} 
 \begin{center}
 \begin{tabular}{rrr} 
-  \it name    	&\it meta-type 		& \it description	\\ 
-  \idx{Trueprop}& $o\To prop$		& coercion to $prop$	\\
-  \idx{Seqof}   & $[o,sobj]\To sobj$  	& singleton sequence	\\
-  \idx{Not}	& $o\To o$		& negation ($\neg$) 	\\
-  \idx{True}	& $o$			& tautology ($\top$) 	\\
-  \idx{False}	& $o$			& absurdity ($\bot$)
+  \it name      &\it meta-type          & \it description       \\ 
+  \idx{Trueprop}& $o\To prop$           & coercion to $prop$    \\
+  \idx{Seqof}   & $[o,sobj]\To sobj$    & singleton sequence    \\
+  \idx{Not}     & $o\To o$              & negation ($\neg$)     \\
+  \idx{True}    & $o$                   & tautology ($\top$)    \\
+  \idx{False}   & $o$                   & absurdity ($\bot$)
 \end{tabular}
 \end{center}
 \subcaption{Constants}
 
 \begin{center}
 \begin{tabular}{llrrr} 
-  \it symbol &\it name	   &\it meta-type & \it precedence & \it description \\
+  \it symbol &\it name     &\it meta-type & \it precedence & \it description \\
   \idx{ALL}  & \idx{All}  & $(\alpha\To o)\To o$ & 10 & 
-	universal quantifier ($\forall$) \\
+        universal quantifier ($\forall$) \\
   \idx{EX}   & \idx{Ex}   & $(\alpha\To o)\To o$ & 10 & 
-	existential quantifier ($\exists$) \\
+        existential quantifier ($\exists$) \\
   \idx{THE} & \idx{The}  & $(\alpha\To o)\To \alpha$ & 10 & 
-	definite description ($\iota$)
+        definite description ($\iota$)
 \end{tabular}
 \end{center}
 \subcaption{Binders} 
@@ -98,7 +98,7 @@
 
 \begin{center}
 \begin{tabular}{rrr} 
-  \it external		& \it internal	& \it description \\ 
+  \it external          & \it internal  & \it description \\ 
   \tt $\Gamma$ |- $\Delta$  &  \tt Trueprop($\Gamma$, $\Delta$) &
         sequent $\Gamma\turn \Delta$ 
 \end{tabular}
@@ -121,15 +121,15 @@
          & | & formula 
 \\[2ex]
  formula & = & \hbox{expression of type~$o$} \\
-	 & | & term " = " term \\
-	 & | & "\ttilde\ " formula \\
-	 & | & formula " \& " formula \\
-	 & | & formula " | " formula \\
-	 & | & formula " --> " formula \\
-	 & | & formula " <-> " formula \\
-	 & | & "ALL~" id~id^* " . " formula \\
-	 & | & "EX~~" id~id^* " . " formula \\
-	 & | & "THE~" id~     " . " formula
+         & | & term " = " term \\
+         & | & "\ttilde\ " formula \\
+         & | & formula " \& " formula \\
+         & | & formula " | " formula \\
+         & | & formula " --> " formula \\
+         & | & formula " <-> " formula \\
+         & | & "ALL~" id~id^* " . " formula \\
+         & | & "EX~~" id~id^* " . " formula \\
+         & | & "THE~" id~     " . " formula
   \end{array}
 \]
 \caption{Grammar of {\tt LK}} \label{lk-grammar}
@@ -166,8 +166,13 @@
 \idx{notL}    $H, $G |- $E, P ==> $H, ~P, $G |- $E
 
 \idx{FalseL}  $H, False, $G |- $E
+\end{ttbox}
 \subcaption{Propositional rules}
+\caption{Rules of {\tt LK}}  \label{lk-rules}
+\end{figure}
 
+\begin{figure} 
+\begin{ttbox}
 \idx{allR}    (!!x.$H|- $E, P(x), $F) ==> $H|- $E, ALL x.P(x), $F
 \idx{allL}    $H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G|- $E
             
@@ -176,10 +181,10 @@
 
 \idx{The}     [| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
         $H |- $E, P(THE x.P(x)), $F
+\end{ttbox}
 \subcaption{Quantifier rules}
-\end{ttbox}
 
-\caption{Rules of {\tt LK}}  \label{lk-rules}
+\caption{Rules of {\tt LK} (continued)}  \label{lk-rules2}
 \end{figure}
 
 
@@ -223,13 +228,13 @@
 as a formula.
 
 The theory has the \ML\ identifier \ttindexbold{LK.thy}.
-Figure~\ref{lk-rules} presents the rules.  The connective $\bimp$ is
-defined using $\conj$ and $\imp$.  The axiom for basic sequents is
-expressed in a form that provides automatic thinning: redundant formulae
-are simply ignored.  The other rules are expressed in the form most
-suitable for backward proof --- they do not require exchange or contraction
-rules.  The contraction rules are actually derivable (via cut) in this
-formulation.
+Figures~\ref{lk-rules} and~\ref{lk-rules2} present the rules.  The
+connective $\bimp$ is defined using $\conj$ and $\imp$.  The axiom for
+basic sequents is expressed in a form that provides automatic thinning:
+redundant formulae are simply ignored.  The other rules are expressed in
+the form most suitable for backward proof --- they do not require exchange
+or contraction rules.  The contraction rules are actually derivable (via
+cut) in this formulation.
 
 Figure~\ref{lk-derived} presents derived rules, including rules for
 $\bimp$.  The weakened quantifier rules discard each quantification after a