src/HOL/Set.thy

--- a/src/HOL/Set.thy	Wed Jul 05 16:50:07 2023 +0100
+++ b/src/HOL/Set.thy	Thu Jul 06 16:59:12 2023 +0100
@@ -719,6 +719,9 @@
 lemma Compl_eq_Diff_UNIV: "- A = (UNIV - A)"
   by blast
 
+abbreviation sym_diff :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "sym_diff A B \<equiv> ((A - B) \<union> (B-A))"
+
 
 subsubsection \<open>Augmenting a set -- \<^const>\<open>insert\<close>\<close>