equal
deleted
inserted
replaced
163 by (lifting DC) |
163 by (lifting DC) |
164 |
164 |
165 subsection{*The Abstract Function to Return the Set of Nonces*} |
165 subsection{*The Abstract Function to Return the Set of Nonces*} |
166 |
166 |
167 quotient_def |
167 quotient_def |
168 nonces :: "nounces:: msg \<Rightarrow> nat set" |
168 nonces :: "nonces:: msg \<Rightarrow> nat set" |
169 where |
169 where |
170 "freenonces" |
170 "freenonces" |
171 |
171 |
172 text{*Now prove the four equations for @{term nonces}*} |
172 text{*Now prove the four equations for @{term nonces}*} |
173 |
173 |