diff -r 1b3385de296d -r 1755b24e8b44 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Mon Feb 02 14:01:33 2015 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Mon Feb 02 14:01:33 2015 +0100
@@ -57,7 +57,7 @@
 subsubsection{*The Set of Nonces*}
 
 text{*A function to return the set of nonces present in a message.  It will
-be lifted to the initial algrebra, to serve as an example of that process.*}
+be lifted to the initial algebra, to serve as an example of that process.*}
 primrec freenonces :: "freemsg \<Rightarrow> nat set" where
   "freenonces (NONCE N) = {N}"
 | "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
@@ -74,7 +74,7 @@
 subsubsection{*The Left Projection*}
 
 text{*A function to return the left part of the top pair in a message.  It will
-be lifted to the initial algrebra, to serve as an example of that process.*}
+be lifted to the initial algebra, to serve as an example of that process.*}
 primrec freeleft :: "freemsg \<Rightarrow> freemsg" where
   "freeleft (NONCE N) = NONCE N"
 | "freeleft (MPAIR X Y) = X"