src/HOL/Library/LaTeXsugar.thy
changeset 16110 c423bb89186d
parent 15690 1da2cfd1ca45
child 19674 22b635240905
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Sun May 29 12:41:40 2005 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon May 30 08:21:58 2005 +0200
     1.3 @@ -20,6 +20,12 @@
     1.4    "_case_syntax":: "['a, cases_syn] => 'b"
     1.5    ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
     1.6  
     1.7 +(* should become standard syntax once x-symbols supports it *)
     1.8 +syntax (latex)
     1.9 +  nexists :: "('a => bool) => bool"           (binder "\<nexists>" 10)
    1.10 +translations
    1.11 +  "\<nexists>x. P" <= "\<not>(\<exists>x. P)"
    1.12 +
    1.13  (* SETS *)
    1.14  
    1.15  (* empty set *)