--- 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