summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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