doc-src/TutorialI/basics.tex
changeset 11301 be4163219703
parent 11213 aeb5c72dd72a
child 11405 b6e3ac38397d
--- a/doc-src/TutorialI/basics.tex	Wed May 16 17:58:48 2001 +0200
+++ b/doc-src/TutorialI/basics.tex	Wed May 16 18:03:12 2001 +0200
@@ -275,8 +275,8 @@
 \section{Interaction and Interfaces}
 
 Interaction with Isabelle can either occur at the shell level or through more
-advanced interfaces. To keep the tutorial independent of the interface we
-have phrased the description of the intraction in a neutral language. For
+advanced interfaces. To keep the tutorial independent of the interface, we
+have phrased the description of the interaction in a neutral language. For
 example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
 shell level, which is explained the first time the phrase is used. Other
 interfaces perform the same act by cursor movements and/or mouse clicks.