changeset 14565 | c6dc17aab88a |
parent 14533 | 32806c0afebf |
child 14658 | b1293d0f8d5f |
--- a/src/HOL/Induct/QuoDataType.thy Wed Apr 14 13:28:46 2004 +0200 +++ b/src/HOL/Induct/QuoDataType.thy Wed Apr 14 14:13:05 2004 +0200 @@ -26,6 +26,8 @@ "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "~~" 50) syntax (xsymbols) "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50) +syntax (HTML output) + "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50) translations "X \<sim> Y" == "(X,Y) \<in> msgrel"