[isabelle-dev] Symmetric difference of sets
lp15 at cam.ac.uk
Wed Sep 18 12:47:16 CEST 2019
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).
More information about the isabelle-dev