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

author | nipkow |

Mon, 10 Feb 2003 15:57:46 +0100 | |

changeset 13814 | 5402c2eaf393 |

parent 13813 | 722593f2f068 |

child 13815 | 0832792725db |

*** empty log message ***

--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Feb 10 09:45:22 2003 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Mon Feb 10 15:57:46 2003 +0100 @@ -50,7 +50,7 @@ It is inadvisable to toggle the simplification attribute of a theorem from a parent theory $A$ in a child theory $B$ for good. The reason is that if some theory $C$ is based both on $B$ and (via a - differnt path) on $A$, it is not defined what the simplification attribute + different path) on $A$, it is not defined what the simplification attribute of that theorem will be in $C$: it could be either. \end{warn}% \end{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/simp.thy Mon Feb 10 09:45:22 2003 +0100 +++ b/doc-src/TutorialI/Misc/simp.thy Mon Feb 10 15:57:46 2003 +0100 @@ -46,7 +46,7 @@ It is inadvisable to toggle the simplification attribute of a theorem from a parent theory $A$ in a child theory $B$ for good. The reason is that if some theory $C$ is based both on $B$ and (via a - differnt path) on $A$, it is not defined what the simplification attribute + different path) on $A$, it is not defined what the simplification attribute of that theorem will be in $C$: it could be either. \end{warn} *}

--- a/doc-src/TutorialI/Sets/sets.tex Mon Feb 10 09:45:22 2003 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Mon Feb 10 15:57:46 2003 +0100 @@ -377,12 +377,12 @@ \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 -\hbox{\isa{Ex\ P}}\index{*Ex (constant)} is \isa{\isasymexists z.\ P\ x}; +\isa{{\isasymforall}x.\ P\ x} and +\hbox{\isa{Ex\ P}}\index{*Ex (constant)} is \isa{\isasymexists x.\ P\ x}; also \isa{Ball\ A\ P}\index{*Ball (constant)} is -\isa{{\isasymforall}z\isasymin A.\ P\ x} and +\isa{{\isasymforall}x\isasymin A.\ P\ x} and \isa{Bex\ A\ P}\index{*Bex (constant)} is -\isa{\isasymexists z\isasymin A.\ P\ x}. For indexed unions and +\isa{\isasymexists x\isasymin A.\ P\ x}. For indexed unions and intersections, you may see the constants \cdx{UNION} and \cdx{INTER}\@. The internal constant for $\varepsilon x.P(x)$ is~\cdx{Eps}.

--- a/doc-src/TutorialI/basics.tex Mon Feb 10 09:45:22 2003 +0100 +++ b/doc-src/TutorialI/basics.tex Mon Feb 10 15:57:46 2003 +0100 @@ -90,7 +90,7 @@ as a direct or indirect parent of all your theories. \end{warn} There is also a growing Library~\cite{HOL-Library}\index{Library} -of useful theories that are not part of \isa{Main} but can to be included +of useful theories that are not part of \isa{Main} but can be included among the parents of a theory and will then be loaded automatically.% \index{theories|)} @@ -161,10 +161,10 @@ \item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions} Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type. \item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions} -is equivalent to $u$ where all occurrences of $x$ have been replaced by +is equivalent to $u$ where all free occurrences of $x$ have been replaced by $t$. For example, \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated -by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}. +by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}. \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}] \index{*case expressions} evaluates to $e@i$ if $e$ is of the form $c@i$.

--- a/doc-src/TutorialI/tutorial.ind Mon Feb 10 09:45:22 2003 +0100 +++ b/doc-src/TutorialI/tutorial.ind Mon Feb 10 15:57:46 2003 +0100 @@ -182,7 +182,7 @@ \item elimination rules, 69--70 \item \isacommand {end} (command), 14 \item \isa {Eps} (constant), 109 - \item equality, 5 + \item equality, 6 \subitem of functions, \bold{109} \subitem of records, 161 \subitem of sets, \bold{106}