summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 05 May 1997 18:50:26 +0200 | |

changeset 3106 | 5396e99c02af |

parent 3105 | 1a5bfa2ab1d1 |

child 3107 | 492a3d5d2b17 |

tuned;

doc-src/Intro/advanced.tex | file | annotate | diff | comparison | revisions | |

doc-src/Intro/foundations.tex | file | annotate | diff | comparison | revisions |

--- a/doc-src/Intro/advanced.tex Mon May 05 18:09:31 1997 +0200 +++ b/doc-src/Intro/advanced.tex Mon May 05 18:50:26 1997 +0200 @@ -368,7 +368,7 @@ theories, inheriting their types, constants, syntax, etc. The theory \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant \thydx{CPure} offers the more usual higher-order function application -syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$. +syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure. Each theory definition must reside in a separate file, whose name is the theory's with {\tt.thy} appended. Calling @@ -429,9 +429,9 @@ the keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are rules of the form $s \equiv t$, and should serve only as abbreviations. The simplest form of a definition is $f \equiv t$, -where $f$ is a constant. Also allowed are $\eta$-equivalent forms, -where the arguments of~$f$ appear applied on the left-hand side of the -equation instead of abstracted on the right-hand side. +where $f$ is a constant. Also allowed are $\eta$-equivalent forms of +this, where the arguments of~$f$ appear applied on the left-hand side +of the equation instead of abstracted on the right-hand side. Isabelle checks for common errors in definitions, such as extra variables on the right-hand side, but currently does not a complete

--- a/doc-src/Intro/foundations.tex Mon May 05 18:09:31 1997 +0200 +++ b/doc-src/Intro/foundations.tex Mon May 05 18:50:26 1997 +0200 @@ -1,4 +1,5 @@ %% $Id$ + \part{Foundations} The following sections discuss Isabelle's logical foundations in detail: representing logical syntax in the typed $\lambda$-calculus; expressing @@ -642,8 +643,8 @@ Resolution expects the rules to have no outer quantifiers~($\Forall$). It may rename or instantiate any schematic variables, but leaves free variables unchanged. When constructing a theory, Isabelle puts the -rules into a standard form containing only schematic variables; -for instance, $({\imp}E)$ becomes +rules into a standard form with all free variables converted into +schematic ones; for instance, $({\imp}E)$ becomes \[ \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}. \] When resolving two rules, the unknowns in the first rule are renamed, by