author | nipkow |

Tue Feb 20 10:37:12 2001 +0100 (2001-02-20) | |

changeset 11159 | 07b13770c4d6 |

parent 11158 | 5652018b809a |

child 11160 | e0ab13bec5c8 |

*** empty log message ***

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

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

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

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

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

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