--- 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
--- 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
--- 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)