[isabelle-dev] Symmetric difference of sets

Lawrence Paulson 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 mailing list