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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
