From 25086947faa4c26966592baa6be788f58393474e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Jan 2014 19:14:11 -0800
Subject: [PATCH] fix(builtin/kernel): incorrect comment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index c31b0d6ac..d03d36809 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -49,7 +49,6 @@ infix 50 ≠ : neq
 theorem em (a : Bool) : a ∨ ¬ a
 := λ Hna : ¬ a, Hna
 
--- Boolean completeness
 axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
 
 axiom refl {A : TypeU} (a : A) : a == a