src/HOL/Library/LaTeXsugar.thy
changeset 56977 a33fe940a557
parent 56245 84fc7dfa3cd4
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Thu May 15 16:46:29 2014 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri May 16 09:19:15 2014 +0200
     1.3 @@ -48,11 +48,15 @@
     1.4    "_Collect p P"      <= "{p|xs. P}"
     1.5    "_CollectIn p A P"  <= "{p : A. P}"
     1.6  
     1.7 +(* card *)
     1.8 +notation (latex output)
     1.9 +  card  ("|_|")
    1.10 +
    1.11  (* LISTS *)
    1.12  
    1.13  (* Cons *)
    1.14  notation (latex)
    1.15 -  Cons  ("_\<cdot>/_" [66,65] 65)
    1.16 +  Cons  ("_ \<cdot>/ _" [66,65] 65)
    1.17  
    1.18  (* length *)
    1.19  notation (latex output)