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.
   If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential
   quantifier, it needs to be followed by a space. Otherwise \isa{?x} is