diff options
| author | Enrico | 2019-01-22 10:25:32 +0100 |
|---|---|---|
| committer | GitHub | 2019-01-22 10:25:32 +0100 |
| commit | c34a49df5ffd3f3975ab3327817d448e638f03d3 (patch) | |
| tree | 86e0ff4ccbb1bc27dc264011eea61c770b24cb47 | |
| parent | 60113af483a6cd98a4b26ae7ee7d76c9380f341d (diff) | |
Update CHANGES.md
| -rw-r--r-- | CHANGES.md | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/CHANGES.md b/CHANGES.md index 3ef0043672..a1ef849d92 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -156,23 +156,23 @@ Misc SSReflect - New intro patterns: - - temporary introduction: => + - - block introduction: => [^ prefix ] [^~ suffix ] - - fast introduction: => > - - tactics as views: => /ltac:mytac - - replace hypothesis: => {}H + - temporary introduction: `=> +` + - block introduction: `=> [^ prefix ] [^~ suffix ]` + - fast introduction: `=> >` + - tactics as views: `=> /ltac:mytac` + - replace hypothesis: `=> {}H` See the reference manual for the actual documentation. - Clear discipline made consistent across the entire proof language. - Whenever a clear switch {x..} comes immediately before an existing proof + Whenever a clear switch `{x..}` comes immediately before an existing proof context entry (used as a view, as a rewrite rule or as name for a new context entry) then such entry is cleared too. E.g. The following sentences are elaborated as follows (when H is an existing proof context entry): - - "=> {x..} H" -> "=> {x..H} H" - - "=> {x..} /H" -> "=> /v {x..H}" - - "rewrite {x..} H" -> "rewrite E {x..H}" + - `=> {x..} H` -> `=> {x..H} H` + - `=> {x..} /H` -> `=> /v {x..H}` + - `rewrite {x..} H` -> `rewrite E {x..H}` Changes from 8.8.2 to 8.9+beta1 =============================== |