michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/logic/examples/colog88): remove unnecessary annotation

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-24 12:45:06 -07:00
parent a5306e70eb
commit 1149ead14c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/logic/examples/colog88.lean
View file

@ -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