# HG changeset patch
# User wenzelm
# Date 789045372 -3600
# Node ID 14b96e3bd4ab2e75e2961a324aa9883250f316ac
# Parent  5716e174b591461bf104427d64e862fb51752571
fixed minor typos;

diff -r 5716e174b591 -r 14b96e3bd4ab doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Mon Jan 02 12:14:26 1995 +0100
+++ b/doc-src/Intro/advanced.tex	Mon Jan 02 12:16:12 1995 +0100
@@ -338,8 +338,8 @@
 types        {\it type declarations and synonyms}
 arities      {\it arity declarations}
 consts       {\it constant declarations}
+translations {\it translation declarations}
 rules        {\it rule declarations}
-translations {\it translation declarations}
 end
 ML           {\it ML code}
 \end{ttbox}
@@ -453,7 +453,7 @@
 \begin{ttbox}
 types   \(tids@1\) \(id@1\)
         \vdots
-        \(tids@1\) \(id@n\)
+        \(tids@n\) \(id@n\)
 \end{ttbox}
 where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
 are type argument lists as shown in the example above.  It declares each
diff -r 5716e174b591 -r 14b96e3bd4ab doc-src/Logics/LK.tex
--- a/doc-src/Logics/LK.tex	Mon Jan 02 12:14:26 1995 +0100
+++ b/doc-src/Logics/LK.tex	Mon Jan 02 12:16:12 1995 +0100
@@ -164,7 +164,7 @@
 \tdx{disjR}   $H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F
 \tdx{disjL}   [| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E
             
-\tdx{impR}    $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $
+\tdx{impR}    $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F
 \tdx{impL}    [| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E
             
 \tdx{notR}    $H, P |- $E, $F ==> $H |- $E, ~P, $F
diff -r 5716e174b591 -r 14b96e3bd4ab doc-src/Logics/Old_HOL.tex
--- a/doc-src/Logics/Old_HOL.tex	Mon Jan 02 12:14:26 1995 +0100
+++ b/doc-src/Logics/Old_HOL.tex	Mon Jan 02 12:16:12 1995 +0100
@@ -604,7 +604,7 @@
 \tdx{mem_Collect_eq}    (a : \{x.P(x)\}) = P(a)
 \tdx{Collect_mem_eq}    \{x.x:A\} = A
 
-\tdx{empty_def}         \{\}          == \{x.x=False\}
+\tdx{empty_def}         \{\}          == \{x.False\}
 \tdx{insert_def}        insert(a,B) == \{x.x=a\} Un B
 \tdx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
 \tdx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)