# 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.