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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
