--- a/src/Doc/Implementation/ML.thy Tue Dec 23 21:14:44 2014 +0100
+++ b/src/Doc/Implementation/ML.thy Wed Dec 24 10:06:37 2014 +0100
@@ -1835,7 +1835,7 @@
Isabelle environment. User code should not break this abstraction, but stay
within the confines of concurrent Isabelle/ML.
- A \emph{synchronized variable} is an explicit state component is associated
+ A \emph{synchronized variable} is an explicit state component associated
with mechanisms for locking and signaling. There are operations to await a
condition, change the state, and signal the change to all other waiting
threads. Synchronized access to the state variable is \emph{not} re-entrant:
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Dec 23 21:14:44 2014 +0100
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Wed Dec 24 10:06:37 2014 +0100
@@ -75,7 +75,7 @@
Now you need to learn what to type into it.
\else
If you want to apply what you have learned about Isabelle we recommend you
-donwload and read the book
+download and read the book
\href{http://www.concrete-semantics.org}{Concrete
Semantics}~\cite{ConcreteSemantics}, a guided tour of the wonderful world of
programming langage semantics formalised in Isabelle. In fact,