summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/basics.tex

changeset 9689 | 751fde5307e4 |

parent 9541 | d17c0b34d5c8 |

child 9792 | bbefb6ce5cb2 |

--- a/doc-src/TutorialI/basics.tex Fri Aug 25 12:17:09 2000 +0200 +++ b/doc-src/TutorialI/basics.tex Mon Aug 28 09:32:51 2000 +0200 @@ -256,6 +256,7 @@ 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. +Note that for readability we often drop the \isa{?}s when displaying a theorem. \begin{warn} If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential quantifier, it needs to be followed by a space. Otherwise \isa{?x} is