Leonardo de Moura f7fe2a775c feat(library/init/meta/rewrite_tactic): improve rewrite tactic ... `rewrite` tactic improvements - Add support for `auto_param` and `opt_param` - Order new goals using the same strategies available for `apply` - Allow user to set configuration object in interactive mode. @Armael This commit should address the issue you raised about the order of new goals in the `rewrite` tactic. See new test tests/lean/run/rw1.lean for examples.		2017-06-30 12:03:27 -07:00
..
algebra	feat(init/data/int): int lemmas, more bitwise theorems	2017-06-27 18:55:52 -07:00
category	refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let	2017-06-22 08:03:23 -07:00
data	refactor(init/data/nat/gcd): define gcd using eqn compiler	2017-06-27 18:55:52 -07:00
meta	feat(library/init/meta/rewrite_tactic): improve rewrite tactic	2017-06-30 12:03:27 -07:00
native	refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let	2017-06-22 08:03:23 -07:00
cc_lemmas.lean	feat(frontends/lean): use . for field access	2017-03-28 15:29:54 -07:00
classical.lean	fix(library/noncomputable): fixes #1631	2017-05-31 23:16:37 -07:00
coe.lean	chore(library): convert comments to docstrings	2017-06-12 15:17:00 +02:00
core.lean	chore(library): convert comments to docstrings	2017-06-12 15:17:00 +02:00
default.lean	feat(library/init/meta/well_founded_tactics): add simple tactic for discharging decreasing proofs	2017-05-23 22:07:46 -07:00
function.lean	chore(library/init): remove reducible annotations for id, const, etc, and move $ notation to core.lean	2017-03-11 11:34:16 -08:00
funext.lean	refactor(init/funext): shorten proof	2017-05-27 04:13:59 -04:00
init.md	chore(*.md): fix/remove broken links	2016-02-23 10:11:24 -08:00
logic.lean	chore(library): convert comments to docstrings	2017-06-12 15:17:00 +02:00
propext.lean	feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term	2017-03-28 17:47:49 -07:00
relator.lean	feat(init/relator): some new base theorems for transfer tactic	2017-05-27 04:16:25 -04:00
util.lean	refactor(library): has_to_string ==> has_repr	2017-06-18 18:29:19 -07:00
wf.lean	feat(library/init): use Sort instead of Type for defining acc and well_founded	2017-05-23 16:40:45 -07:00