Leonardo de Moura c3d4a9456e feat(library/init/meta/interactive): add sorry interactive tactic (alias for admit).		2018-01-11 16:58:46 -08:00
..
lean	feat(library/init/meta/interactive): add sorry interactive tactic (alias for admit).	2018-01-11 16:58:46 -08:00
.gitignore