[isabelle-dev] Symmetric difference of sets

[Lawrence Paulson]

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