doc-src/TutorialI/basics.tex

 \end{warn}
 
 \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.
 Although shell-based interaction is quite feasible for the kind of proof
 scripts currently presented in this tutorial, the recommended interface for