--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Mon Feb 02 14:01:33 2015 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Mon Feb 02 14:01:33 2015 +0100
@@ -62,7 +62,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