# HG changeset patch
# User paulson
# Date 990028992 -7200
# Node ID be41632197036bacc62b9e9c9e15b726ada25bff
# Parent  5b6887aedc7676e1adc24f8f96ba7e91ac0b364f
spelling

diff -r 5b6887aedc76 -r be4163219703 doc-src/TutorialI/basics.tex
--- 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.