doc-src/TutorialI/basics.tex
changeset 13439 2f98365f57a8
parent 12668 b839bd6e06c6
child 13814 5402c2eaf393
--- a/doc-src/TutorialI/basics.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/basics.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -281,7 +281,7 @@
 variables are automatically renamed to avoid clashes with free variables. In
 addition, Isabelle has a third kind of variable, called a \textbf{schematic
   variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, 
-which must a~\isa{?} as its first character.  
+which must have a~\isa{?} as its first character.  
 Logically, an unknown is a free variable. But it may be
 instantiated by another term during the proof process. For example, the
 mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},