[isabelle-dev] Symmetric difference of sets

[Tobias Nipkow]

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.

Tobias

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>