added \nexists
authornipkow
Mon May 30 08:21:58 2005 +0200 (2005-05-30)
changeset 16110c423bb89186d
parent 16109 e8c169d6f191
child 16111 d06dc7975731
added \nexists
lib/texinputs/isabellesym.sty
src/HOL/Library/LaTeXsugar.thy
     1.1 --- a/lib/texinputs/isabellesym.sty	Sun May 29 12:41:40 2005 +0200
     1.2 +++ b/lib/texinputs/isabellesym.sty	Mon May 30 08:21:58 2005 +0200
     1.3 @@ -220,6 +220,7 @@
     1.4  \newcommand{\isasymOr}{\isamath{\bigvee}}
     1.5  \newcommand{\isasymforall}{\isamath{\forall\,}}
     1.6  \newcommand{\isasymexists}{\isamath{\exists\,}}
     1.7 +\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
     1.8  \newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
     1.9  \newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
    1.10  \newcommand{\isasymturnstile}{\isamath{\vdash}}
     2.1 --- a/src/HOL/Library/LaTeXsugar.thy	Sun May 29 12:41:40 2005 +0200
     2.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon May 30 08:21:58 2005 +0200
     2.3 @@ -20,6 +20,12 @@
     2.4    "_case_syntax":: "['a, cases_syn] => 'b"
     2.5    ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
     2.6  
     2.7 +(* should become standard syntax once x-symbols supports it *)
     2.8 +syntax (latex)
     2.9 +  nexists :: "('a => bool) => bool"           (binder "\<nexists>" 10)
    2.10 +translations
    2.11 +  "\<nexists>x. P" <= "\<not>(\<exists>x. P)"
    2.12 +
    2.13  (* SETS *)
    2.14  
    2.15  (* empty set *)