Leonardo de Moura
|
5cf8064269
|
refactor(library): rename exists_elim and exists_intro to exists.elim
and exists.intro
|
2014-12-15 19:07:38 -08:00 |
|
Jeremy Avigad
|
3e9a484851
|
refactor(library/logic/connectives): rename theorems
|
2014-12-15 15:05:44 -05:00 |
|
Floris van Doorn
|
c630b5ddb2
|
feat(library/algebra/category): use variables instead of parameters
|
2014-10-11 16:40:18 -07:00 |
|
Leonardo de Moura
|
6632a50015
|
refactor(library): add namespaces 'or', 'and' and 'iff'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 21:25:21 -07:00 |
|
Leonardo de Moura
|
2bc6f92d33
|
refactor(library): add 'and' namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 17:44:53 -07:00 |
|
Leonardo de Moura
|
364bba2129
|
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 17:26:36 -07:00 |
|
Leonardo de Moura
|
2d78387541
|
refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-27 18:34:09 -07:00 |
|
Leonardo de Moura
|
a8d58fdd33
|
refactor(library): mark absurd_elim argument as implicit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-26 18:27:39 -07:00 |
|
Leonardo de Moura
|
dbaf81e16d
|
refactor(library): remove unnecessary 'standard' subdirectory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-23 18:08:09 -07:00 |
|