src/HOL/Library/LaTeXsugar.thy
changeset 21210 c17fd2df4e9e
parent 19674 22b635240905
child 22328 cc403d881873
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  begin
     1.5  
     1.6  (* LOGIC *)
     1.7 -const_syntax (latex output)
     1.8 +notation (latex output)
     1.9    If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
    1.10  
    1.11  syntax (latex output)
    1.12 @@ -52,15 +52,15 @@
    1.13  (* LISTS *)
    1.14  
    1.15  (* Cons *)
    1.16 -const_syntax (latex)
    1.17 +notation (latex)
    1.18    Cons  ("_\<cdot>/_" [66,65] 65)
    1.19  
    1.20  (* length *)
    1.21 -const_syntax (latex output)
    1.22 +notation (latex output)
    1.23    length  ("|_|")
    1.24  
    1.25  (* nth *)
    1.26 -const_syntax (latex output)
    1.27 +notation (latex output)
    1.28    nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    1.29  
    1.30  (* DUMMY *)