doc-src/Intro/foundations.tex
 changeset 9695 ec7d7f877712 parent 6592 c120262044b6 child 42637 381fdcab0f36
--- a/doc-src/Intro/foundations.tex	Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/Intro/foundations.tex	Mon Aug 28 13:52:38 2000 +0200
@@ -441,20 +441,18 @@
Under similar conditions, a signature can be extended.  Signatures are
managed internally by Isabelle; users seldom encounter them.

-\index{theories|bold} A {\bf theory} consists of a signature plus a
-collection of axioms.  The {\Pure} theory contains only the
-meta-logic.  Theories can be combined provided their signatures are
-compatible.  A theory definition extends an existing theory with
-further signature specifications --- classes, types, constants and
-mixfix declarations --- plus lists of axioms and definitions etc.,
-expressed as strings to be parsed.  A theory can formalize a small
-piece of mathematics, such as lists and their operations, or an entire
-logic.  A mathematical development typically involves many theories in
-a hierarchy.  For example, the {\Pure} theory could be extended to
-form a theory for Fig.\ts\ref{fol-fig}; this could be extended in two
-separate ways to form a theory for natural numbers and a theory for
-lists; the union of these two could be extended into a theory defining
-the length of a list:
+\index{theories|bold} A {\bf theory} consists of a signature plus a collection
+of axioms.  The Pure theory contains only the meta-logic.  Theories can be
+combined provided their signatures are compatible.  A theory definition
+extends an existing theory with further signature specifications --- classes,
+types, constants and mixfix declarations --- plus lists of axioms and
+definitions etc., expressed as strings to be parsed.  A theory can formalize a
+small piece of mathematics, such as lists and their operations, or an entire
+logic.  A mathematical development typically involves many theories in a
+hierarchy.  For example, the Pure theory could be extended to form a theory
+for Fig.\ts\ref{fol-fig}; this could be extended in two separate ways to form
+a theory for natural numbers and a theory for lists; the union of these two
+could be extended into a theory defining the length of a list:
\begin{tt}
\[
\begin{array}{c@{}c@{}c@{}c@{}c}