--- 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"