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

author | nipkow |

Tue, 20 Feb 2001 10:37:12 +0100 | |

changeset 11159 | 07b13770c4d6 |

parent 11158 | 5652018b809a |

child 11160 | e0ab13bec5c8 |

*** empty log message ***

--- a/doc-src/TutorialI/Recdef/Induction.thy Tue Feb 20 10:18:26 2001 +0100 +++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Feb 20 10:37:12 2001 +0100 @@ -47,7 +47,7 @@ In general, the format of invoking recursion induction is \begin{quote} -\isacommand{apply}@{text"(induct_tac "}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"} +\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"} \end{quote}\index{*induct_tac}% where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the name of a function that takes an $n$-tuple. Usually the subgoal will

--- a/doc-src/TutorialI/Recdef/document/Induction.tex Tue Feb 20 10:18:26 2001 +0100 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Feb 20 10:37:12 2001 +0100 @@ -49,7 +49,7 @@ In general, the format of invoking recursion induction is \begin{quote} -\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac}$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} +\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} \end{quote}\index{*induct_tac}% where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the name of a function that takes an $n$-tuple. Usually the subgoal will

--- a/doc-src/TutorialI/Rules/rules.tex Tue Feb 20 10:18:26 2001 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Tue Feb 20 10:37:12 2001 +0100 @@ -570,7 +570,7 @@ placeholders for terms. \emph{Unification} refers to the process of making two terms identical, possibly by replacing their schematic variables by terms. The simplest case is when the two terms are already the same. Next -simplest is when the variables in only one of the term +simplest is when the variables in only one of the terms are replaced; this is called pattern-matching. The \isa{rule} method typically matches the rule's conclusion against the current subgoal. In the most complex case, variables in both @@ -655,7 +655,7 @@ resulting subgoal is trivial by assumption, so the \isacommand{by} command proves it implicitly. -We are using the \isa{erule} method it in a novel way. Hitherto, +We are using the \isa{erule} method in a novel way. Hitherto, the conclusion of the rule was just a variable such as~\isa{?R}, but it may be any term. The conclusion is unified with the subgoal just as it would be with the \isa{rule} method. At the same time \isa{erule} looks

--- a/doc-src/TutorialI/Sets/sets.tex Tue Feb 20 10:18:26 2001 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Tue Feb 20 10:37:12 2001 +0100 @@ -374,7 +374,7 @@ \isa{Collect},\index{*Collect (constant)} which occasionally appears when a goal or theorem is displayed. For example, \isa{Collect\ P} is the same term as -\isa{\isacharbraceleft z.\ P\ x\isacharbraceright}. The same thing can +\isa{\isacharbraceleft x.\ P\ x\isacharbraceright}. The same thing can happen with quantifiers: \hbox{\isa{All\ P}}\index{*All (constant)} is \isa{{\isasymforall}z.\ P\ x} and

--- a/doc-src/TutorialI/appendix.tex Tue Feb 20 10:18:26 2001 +0100 +++ b/doc-src/TutorialI/appendix.tex Tue Feb 20 10:37:12 2001 +0100 @@ -53,7 +53,7 @@ \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} & \verb$\<exists>!$\\ \indexboldpos{\isasymepsilon}{$HOL0ExSome} & -\ttindexbold{SOME} & +\ttindexbold{SOME}, \texttt{\at}\index{$HOL2list@\texttt{\at}} & \verb$\<epsilon>$\\ \indexboldpos{\isasymcirc}{$HOL1} & \ttindexbold{o} &

--- a/doc-src/TutorialI/fp.tex Tue Feb 20 10:18:26 2001 +0100 +++ b/doc-src/TutorialI/fp.tex Tue Feb 20 10:37:12 2001 +0100 @@ -297,7 +297,7 @@ Simplification is one of the central theorem proving tools in Isabelle and many other systems. The tool itself is called the \bfindex{simplifier}. The -purpose of this section is introduce the many features of the simplifier. +purpose of this section is to introduce the many features of the simplifier. Anybody intending to perform proofs in HOL should read this section. Later on ({\S}\ref{sec:simplification-II}) we explain some more advanced features and a little bit of how the simplifier works. The serious student should read that @@ -466,7 +466,7 @@ defined by means of \isacommand{recdef}: you can use full pattern-matching, recursion need not involve datatypes, and termination is proved by showing that the arguments of all recursive calls are smaller in a suitable (user -supplied) sense. In this section we ristrict ourselves to measure functions; +supplied) sense. In this section we restrict ourselves to measure functions; more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}. \subsection{Defining Recursive Functions}