Skip to content

Commit

Permalink
Correct minor error in release notes
Browse files Browse the repository at this point in the history
  • Loading branch information
mn200 committed Oct 10, 2023
1 parent 10d9569 commit 502a460
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/next-release.md
Original file line number Diff line number Diff line change
Expand Up @@ -196,7 +196,7 @@ Incompatibilities:
(With the `Definition` syntax, this is done by using the `schematic` attribute.)
This brings this flavour of definition into line with the others, where the presence of extra free variables on the RHS of a definition’s equation is usually flagged as an error.

* In `real_topologyTheory`, some definitions (only the theorem names but the
* In `real_topologyTheory`, some definitions (only the theorem names but not the
underlying logical constants) have been renamed to avoid conflicts with
similar definitions in `seqTheory`: from `sums` to `sums_def`, from
`summable` to `summable_def`. Besides, `infsum` has been renamed to
Expand Down

0 comments on commit 502a460

Please sign in to comment.