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