From 092fc89333160661c4c5a6295f3054cafff4341e Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 28 Jul 2017 21:54:27 +0100 Subject: [PATCH] doc(changes): changelog --- doc/changes.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/doc/changes.md b/doc/changes.md index c24d4d7bd0..f601c03a11 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -47,6 +47,9 @@ master branch (aka work in progress branch) There is a coercion from `bin_tree` to `list`. The new notation allows to input long sequences efficiently. It also prevents system stack overflows. +* Tactics that accept a location parameter, like `rw thm at h`, may now use `⊢` or the ASCII version `|-` + to select the goal as well as any hypotheses, for example `rw thm at h1 h2 ⊢`. + *Changes* * We now have two type classes for converting to string: `has_to_string` and `has_repr`. @@ -98,6 +101,9 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ * Merged `generalize` and `generalize2` tactics into new `generalize id? : expr = id` tactic +* `standard.lean` has been removed. Any files that `import standard` can simply remove the line as + most things that were once imported by this are now imported by default. + *API name changes* * `list.dropn` => `list.drop` @@ -200,4 +206,4 @@ The available commands can be found [here](https://github.com/leanprover/lean/bl * GCC 7 compatibility -* Use single quotes for character literals (e.g., 'a'). +* Use single quotes for character literals (e.g., 'a'). \ No newline at end of file