[isabelle-dev] Symmetric difference of sets
nipkow at in.tum.de
Wed Sep 18 15:05:48 CEST 2019
This notation is common but not completely standard and the operator is not
frequently used in practice. Hence I would not put it in Main.
On 18/09/2019 12:47, Lawrence Paulson wrote:
> In the AFP entry Ergodic_Theory/SG_Library_Complement we have
> abbreviation sym_diff :: "'a set ⇒ 'a set ⇒ 'a set" (infixl "Δ" 70) where
> "sym_diff A B ≡ ((A - B) ∪ (B-A))”
> I would never use an abbreviation here, due to the repetition of variables, but the primitive itself seems fundamental. Is it worth adding to basic HOL? And even with a symbol (something tells me that Δ is both non-standard and too important to lock up).
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev