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

author | nipkow |

Wed, 02 Aug 2000 13:17:11 +0200 | |

changeset 9494 | 44fefb6e9994 |

parent 9493 | 494f8cd34df7 |

child 9495 | af1fd424941e |

*** empty log message ***

--- a/doc-src/TutorialI/Misc/asm_simp.thy Wed Aug 02 11:30:38 2000 +0200 +++ b/doc-src/TutorialI/Misc/asm_simp.thy Wed Aug 02 13:17:11 2000 +0200 @@ -33,11 +33,13 @@ text{*\noindent There are three options that influence the treatment of assumptions: \begin{description} -\item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored. -\item[\isaindexbold{(no_asm_simp)}] means that the assumptions are not simplified but +\item[\isa{(no_asm)}]\indexbold{*no_asm} + means that assumptions are completely ignored. +\item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp} + means that the assumptions are not simplified but are used in the simplification of the conclusion. -\item[\isaindexbold{(no_asm_use)}] means that the assumptions are simplified -but are not +\item[\isa{(no_asm_use)}]\indexbold{*no_asm_use} + means that the assumptions are simplified but are not used in the simplification of each other or the conclusion. \end{description} Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above

--- a/doc-src/TutorialI/Misc/document/asm_simp.tex Wed Aug 02 11:30:38 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/asm_simp.tex Wed Aug 02 13:17:11 2000 +0200 @@ -29,11 +29,13 @@ \noindent There are three options that influence the treatment of assumptions: \begin{description} -\item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored. -\item[\isaindexbold{(no_asm_simp)}] means that the assumptions are not simplified but +\item[\isa{(no_asm)}]\indexbold{*no_asm} + means that assumptions are completely ignored. +\item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp} + means that the assumptions are not simplified but are used in the simplification of the conclusion. -\item[\isaindexbold{(no_asm_use)}] means that the assumptions are simplified -but are not +\item[\isa{(no_asm_use)}]\indexbold{*no_asm_use} + means that the assumptions are simplified but are not used in the simplification of each other or the conclusion. \end{description} Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above

--- a/doc-src/TutorialI/Misc/document/fakenat.tex Wed Aug 02 11:30:38 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Wed Aug 02 13:17:11 2000 +0200 @@ -2,8 +2,8 @@ % \begin{isamarkuptext}% \noindent -The type \isaindexbold{nat} of natural numbers is predefined and -behaves like% +The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural +numbers is predefined and behaves like% \end{isamarkuptext}% \isacommand{datatype}~nat~=~{"}0{"}~|~Suc~nat\end{isabelle}% %%% Local Variables:

--- a/doc-src/TutorialI/Misc/fakenat.thy Wed Aug 02 11:30:38 2000 +0200 +++ b/doc-src/TutorialI/Misc/fakenat.thy Wed Aug 02 13:17:11 2000 +0200 @@ -3,8 +3,8 @@ (*>*) text{*\noindent -The type \isaindexbold{nat} of natural numbers is predefined and -behaves like +The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural +numbers is predefined and behaves like *} datatype nat = "0" | Suc nat

--- a/doc-src/TutorialI/ToyList/ToyList.thy Wed Aug 02 11:30:38 2000 +0200 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Wed Aug 02 13:17:11 2000 +0200 @@ -220,8 +220,9 @@ text{* \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}} -After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type -\isacommand{oops}) we start a new proof: +After abandoning the above proof attempt\indexbold{abandon +proof}\indexbold{proof!abandon} (at the shell level type +\isacommand{oops}\indexbold{*oops}) we start a new proof: *} lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Aug 02 11:30:38 2000 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Aug 02 13:17:11 2000 +0200 @@ -209,8 +209,9 @@ \begin{isamarkuptext}% \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}} -After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type -\isacommand{oops}) we start a new proof:% +After abandoning the above proof attempt\indexbold{abandon +proof}\indexbold{proof!abandon} (at the shell level type +\isacommand{oops}\indexbold{*oops}) we start a new proof:% \end{isamarkuptext}% \isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}% \begin{isamarkuptxt}%

--- a/doc-src/TutorialI/fp.tex Wed Aug 02 11:30:38 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Wed Aug 02 13:17:11 2000 +0200 @@ -125,7 +125,8 @@ \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. If you suddenly discover that you need to modify a parent theory of your - current theory you must first abandon your current theory (at the shell + current theory you must first abandon your current theory\indexbold{abandon + theory}\indexbold{theory!abandon} (at the shell level type \isacommand{kill}\indexbold{*kill}). After the parent theory has been modified you go back to your original theory. When its first line \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the @@ -316,21 +317,22 @@ see~\S\ref{nat-numerals}. \begin{warn} - The operations \ttindexboldpos{+}{$HOL2arithfun}, - \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun}, - \isaindexbold{min}, \isaindexbold{max}, + The constant \ttindexbold{0} and the operations + \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, + \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available not just for natural numbers but at other types as well (see - \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+y = y+x}, - there is nothing to indicate that you are talking about natural numbers. - Hence Isabelle can only infer that \isa{x} and \isa{y} are of some - arbitrary type where \isa{+} is declared. As a consequence, you will be - unable to prove the goal (although it may take you some time to realize - what has happened if \texttt{show_types} is not set). In this particular - example, you need to include an explicit type constraint, for example - \isa{x+y = y+(x::nat)}. If there is enough contextual information this may - not be necessary: \isa{x+0 = x} automatically implies \isa{x::nat}. + \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there + is nothing to indicate that you are talking about natural numbers. Hence + Isabelle can only infer that \isa{x} is of some arbitrary type where + \isa{0} and \isa{+} are declared. As a consequence, you will be unable to + prove the goal (although it may take you some time to realize what has + happened if \texttt{show_types} is not set). In this particular example, + you need to include an explicit type constraint, for example \isa{x+0 = + (x::nat)}. If there is enough contextual information this may not be + necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because + \isa{Suc} is not overloaded. \end{warn} Simple arithmetic goals are proved automatically by both \isa{auto}