From 1149ead14c8bce878085bb4cfe36be0d754d2c0b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 Apr 2015 12:45:06 -0700 Subject: [PATCH] chore(library/logic/examples/colog88): remove unnecessary annotation --- library/logic/examples/colog88.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/logic/examples/colog88.lean b/library/logic/examples/colog88.lean index f1cc73238..1532a9ce2 100644 --- a/library/logic/examples/colog88.lean +++ b/library/logic/examples/colog88.lean @@ -89,4 +89,4 @@ lemma P0_x0 : P0 x0 := exists.intro P0 (and.intro fP0_eq not_P0_x0) theorem inconsistent : false := -absurd @P0_x0 @not_P0_x0 +absurd P0_x0 not_P0_x0