# HG changeset patch
# User blanchet
# Date 1422882093 -3600
# Node ID 1755b24e8b441c7385bacbfe3439e70edd87b9f8
# Parent  1b3385de296de0bff9bdc67315110b4a13e7c161
fixed typos

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"
diff -r 1b3385de296d -r 1755b24e8b44 src/HOL/Induct/QuoNestedDataType.thy
--- 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" 
diff -r 1b3385de296d -r 1755b24e8b44 src/HOL/Quotient_Examples/Quotient_Message.thy
--- 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