--- 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"
--- a/src/HOL/Induct/QuoNestedDataType.thy Mon Feb 02 14:01:33 2015 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy Mon Feb 02 14:01:33 2015 +0100
@@ -72,7 +72,7 @@
subsubsection{*The Set of Variables*}
text{*A function to return the set of variables 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.
Note that the "free" refers to the free datatype rather than to the concept
of a free variable.*}
primrec freevars :: "freeExp \<Rightarrow> nat set"
--- 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