# HG changeset patch
# User haftmann
# Date 1419411997 -3600
# Node ID 5a783837b50b62615ff3ea2278a894d62372ce66
# Parent  45e31a196b5702bee1199f4c288e0f2c67a7c526
typos

diff -r 45e31a196b57 -r 5a783837b50b src/Doc/Implementation/ML.thy
--- 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:
diff -r 45e31a196b57 -r 5a783837b50b src/Doc/Prog_Prove/document/intro-isabelle.tex
--- 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,