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

author | nipkow |

Fri, 21 May 1999 12:11:13 +0200 | |

changeset 6691 | 8a1b5f9d8420 |

parent 6690 | acbcf8085166 |

child 6692 | 05c56f41e661 |

qed indexed.

doc-src/Tutorial/basics.tex | file | annotate | diff | comparison | revisions | |

doc-src/Tutorial/fp.tex | file | annotate | diff | comparison | revisions |

--- a/doc-src/Tutorial/basics.tex Fri May 21 11:48:42 1999 +0200 +++ b/doc-src/Tutorial/basics.tex Fri May 21 12:11:13 1999 +0200 @@ -245,9 +245,10 @@ Most of the time you can and should ignore unknowns and work with ordinary variables. Just don't be surprised that after you have finished the -proof of a theorem, Isabelle will turn your free variables into unknowns: it -merely indicates that Isabelle will automatically instantiate those unknowns -suitably when the theorem is used in some other proof. +proof of a theorem, Isabelle (i.e.\ \ttindex{qed} at the end of a proof) will +turn your free variables into unknowns: it merely indicates that Isabelle will +automatically instantiate those unknowns suitably when the theorem is used in +some other proof. \begin{warn} The existential quantifier \texttt{?}\index{$HOLQ@{\tt?}} needs to be followed by a space. Otherwise \texttt{?x} is interpreted as a schematic

--- a/doc-src/Tutorial/fp.tex Fri May 21 11:48:42 1999 +0200 +++ b/doc-src/Tutorial/fp.tex Fri May 21 12:11:13 1999 +0200 @@ -219,7 +219,7 @@ \end{ttbox} Now we can give the lemma just proved a suitable name \begin{ttbox} -\input{ToyList/qed2}\end{ttbox} +\input{ToyList/qed2}\end{ttbox}\index{*qed} and tell Isabelle to use this lemma in all future proofs by simplification: \begin{ttbox} \input{ToyList/addsimps2}\end{ttbox} @@ -854,7 +854,7 @@ is like \verb$Simp_tac$, but extracts additional rewrite rules from the assumptions of the subgoal. For example, it solves \begin{ttbox}\makeatother -{\out 1. xs = [] ==> xs @ xs = xs} +{\out 1. xs = [] ==> xs @ ys = ys @ xs} \end{ttbox} which \texttt{Simp_tac} does not do.