# HG changeset patch
# User huffman
# Date 1323636860 -3600
# Node ID 5edf7a15ff8e60dfe5ecf1391240bbde22e79b80
# Parent  0b02adadf38417e35f3a3eff97f3ad23c235b6de
fix spelling

diff -r 0b02adadf384 -r 5edf7a15ff8e doc-src/IsarOverview/Isar/document/intro.tex
--- a/doc-src/IsarOverview/Isar/document/intro.tex	Sun Dec 11 18:22:06 2011 +0100
+++ b/doc-src/IsarOverview/Isar/document/intro.tex	Sun Dec 11 21:54:20 2011 +0100
@@ -116,7 +116,7 @@
 is possible because Isar allows \isa{apply}-style proofs as components
 of structured ones.
 
-Finally, do not be mislead by the simplicity of the formulae being proved,
+Finally, do not be misled by the simplicity of the formulae being proved,
 especially in the beginning. Isar has been used very successfully in
 large applications, for example the formalisation of Java
 dialects~\cite{KleinN-TOPLAS}.