src/HOL/Induct/QuoDataType.thy
changeset 21210 c17fd2df4e9e
parent 19736 d8d0f8f51d69
child 21404 eb85850d3eb7
--- a/src/HOL/Induct/QuoDataType.thy	Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Tue Nov 07 11:47:57 2006 +0100
@@ -26,9 +26,9 @@
   msg_rel :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)
   "X ~~ Y == (X,Y) \<in> msgrel"
 
-const_syntax (xsymbols)
+notation (xsymbols)
   msg_rel  (infixl "\<sim>" 50)
-const_syntax (HTML output)
+notation (HTML output)
   msg_rel  (infixl "\<sim>" 50)
 
 text{*The first two rules are the desired equations. The next four rules