We might also consider the negations of \in, \subseteq, \subset and even perhaps < and > Larry
> On 5 Mar 2016, at 22:19, Makarius <makar...@sketis.net> wrote: > > * New abbreviations for negated existence (but not bounded existence): > > ∄x. P x ≡ ¬ (∃x. P x) > ∄!x. P x ≡ ¬ (∃!x. P x) _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
