equal
deleted
inserted
replaced
254 Most of the time you can and should ignore unknowns and work with ordinary |
254 Most of the time you can and should ignore unknowns and work with ordinary |
255 variables. Just don't be surprised that after you have finished the proof of |
255 variables. Just don't be surprised that after you have finished the proof of |
256 a theorem, Isabelle will turn your free variables into unknowns: it merely |
256 a theorem, Isabelle will turn your free variables into unknowns: it merely |
257 indicates that Isabelle will automatically instantiate those unknowns |
257 indicates that Isabelle will automatically instantiate those unknowns |
258 suitably when the theorem is used in some other proof. |
258 suitably when the theorem is used in some other proof. |
|
259 Note that for readability we often drop the \isa{?}s when displaying a theorem. |
259 \begin{warn} |
260 \begin{warn} |
260 If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential |
261 If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential |
261 quantifier, it needs to be followed by a space. Otherwise \isa{?x} is |
262 quantifier, it needs to be followed by a space. Otherwise \isa{?x} is |
262 interpreted as a schematic variable. |
263 interpreted as a schematic variable. |
263 \end{warn} |
264 \end{warn} |