From 502a460e28085f1c377b422c8c5f95e30dee25be Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 10 Oct 2023 11:30:07 +1100 Subject: [PATCH] Correct minor error in release notes --- doc/next-release.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/next-release.md b/doc/next-release.md index 7208763bb5..7eaeff9245 100644 --- a/doc/next-release.md +++ b/doc/next-release.md @@ -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