equal
deleted
inserted
replaced
119 shows "freediscrim U = freediscrim V" |
119 shows "freediscrim U = freediscrim V" |
120 using a by (induct, auto) |
120 using a by (induct, auto) |
121 |
121 |
122 subsection{*The Initial Algebra: A Quotiented Message Type*} |
122 subsection{*The Initial Algebra: A Quotiented Message Type*} |
123 |
123 |
124 quotient msg = freemsg / msgrel |
124 quotient_type msg = freemsg / msgrel |
125 by (rule equiv_msgrel) |
125 by (rule equiv_msgrel) |
126 |
126 |
127 text{*The abstract message constructors*} |
127 text{*The abstract message constructors*} |
128 |
128 |
129 quotient_def |
129 quotient_def |