From 63a17a3f484b631779433ccb5ea1460ef6f71b08 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <jhendrix@galois.com>
Date: Sun, 29 Nov 2015 23:06:06 -0800
Subject: [PATCH] feat(library/data/bool): Add bxor definition

---
 library/data/bool.lean | 2 ++
 1 file changed, 2 insertions(+)

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