[isabelle-dev] Symmetric difference of sets

Tobias Nipkow 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).
> Larry
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190918/875457a2/attachment.bin>

More information about the isabelle-dev mailing list