summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Mon, 02 Feb 2015 14:01:33 +0100 | |

changeset 59478 | 1755b24e8b44 |

parent 59477 | 1b3385de296d |

child 59479 | b36379a730f4 |

fixed typos

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