summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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}