*** empty log message ***
authornipkow
Tue Feb 20 10:37:12 2001 +0100 (2001-02-20)
changeset 1115907b13770c4d6
parent 11158 5652018b809a
child 11160 e0ab13bec5c8
*** empty log message ***
doc-src/TutorialI/Recdef/Induction.thy
doc-src/TutorialI/Recdef/document/Induction.tex
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/fp.tex
     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}