changeset 766 | df053507edba |
parent 723 | 93dce7c71929 |
child 767 | 37285ec4387d |
--- a/Quot/Examples/LarryDatatype.thy Sun Dec 20 00:15:40 2009 +0100 +++ b/Quot/Examples/LarryDatatype.thy Sun Dec 20 00:26:53 2009 +0100 @@ -121,7 +121,7 @@ subsection{*The Initial Algebra: A Quotiented Message Type*} -quotient msg = freemsg / msgrel +quotient_type msg = freemsg / msgrel by (rule equiv_msgrel) text{*The abstract message constructors*}