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