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