From 10f2dd9992271b0f0ce25e4e1921ffaff2a2f095 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 29 Oct 2020 10:58:11 +0100 Subject: [PATCH] Remove space. --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 87f5d393..3dded487 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -196,7 +196,7 @@ Changes: - Make `gset` a `Definition` instead of a `Notation` to improve performance. - Use `disj_union` (notation `⊎`) for disjoint union on multisets (that adds the multiplicities). Repurpose `∪` on multisets for the actual union (that takes - the max of the multiplicities). + the max of the multiplicities). Naming: -- GitLab