Leonardo de Moura 458958b9fc feat(kernel/inductive): use ih to name induction hypothesis (instead of ih_1) when there is only one		2017-12-05 13:50:24 -08:00
..
basic.lean	feat(library/init/meta/interactive): add iterate n { t }	2017-12-05 12:52:18 -08:00
default.lean	feat(library/data/rbtree): cleanup and add min max	2017-11-18 12:22:10 -08:00
find.lean	feat(library/init/meta/interactive): add iterate n { t }	2017-12-05 12:52:18 -08:00
insert.lean	feat(library/init/meta/interactive): add iterate n { t }	2017-12-05 12:52:18 -08:00
main.lean	feat(kernel/inductive): use ih to name induction hypothesis (instead of ih_1) when there is only one	2017-12-05 13:50:24 -08:00
min_max.lean	fix(library/tactic/cases_tactic): try to clear input hypothesis when performing dependent elimination	2017-12-05 11:03:46 -08:00