[isabelle-dev] NEWS: HOL notation

Lawrence Paulson lp15 at cam.ac.uk
Sun Mar 6 19:25:45 CET 2016


We might also consider the negations of \in, \subseteq, \subset and even perhaps < and >
Larry

> On 5 Mar 2016, at 22:19, Makarius <makarius at sketis.net> wrote:
> 
> * New abbreviations for negated existence (but not bounded existence):
> 
>  ∄x. P x ≡ ¬ (∃x. P x)
>  ∄!x. P x ≡ ¬ (∃!x. P x)




More information about the isabelle-dev mailing list