diff --git a/library/data/bool.lean b/library/data/bool.lean
index 6f2b434c9d..756b8fc6a7 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -127,4 +127,6 @@ namespace bool
 
   theorem eq_ff_of_bnot_eq_tt {a : bool} : bnot a = tt → a = ff :=
   bool.cases_on a (λ h, rfl) (by contradiction)
+
+  definition bxor (x:bool) (y:bool) := cond x (bnot y) y
 end bool