src/HOL/Library/LaTeXsugar.thy
changeset 21210 c17fd2df4e9e
parent 19674 22b635240905
child 22328 cc403d881873
--- a/src/HOL/Library/LaTeXsugar.thy	Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Tue Nov 07 11:47:57 2006 +0100
@@ -10,7 +10,7 @@
 begin
 
 (* LOGIC *)
-const_syntax (latex output)
+notation (latex output)
   If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
 
 syntax (latex output)
@@ -52,15 +52,15 @@
 (* LISTS *)
 
 (* Cons *)
-const_syntax (latex)
+notation (latex)
   Cons  ("_\<cdot>/_" [66,65] 65)
 
 (* length *)
-const_syntax (latex output)
+notation (latex output)
   length  ("|_|")
 
 (* nth *)
-const_syntax (latex output)
+notation (latex output)
   nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
 
 (* DUMMY *)