update CHANGES

Author: fblanqui

Bool.lp

@@ -34,7 +34,7 @@ with istrue false ↪ ⊥;
 
 coerce_rule coerce 𝔹 Prop $x ↪ istrue $x;
 
-symbol istrue=true [x] : π (istrue x) → π (x = true)≔
+symbol istrue=true [x] : π (istrue x) → π (x = true) ≔
 begin
   assume x h;
   refine ∨ₑ (case_𝔹 x) _ _

CHANGES.md

@@ -3,14 +3,23 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
-
 ## Unreleased
 
 ### Added
 
-- FunExt: Axiom for functional extensionality
-- PropExt: Axiom for propositional extensionality and related theorems
-- List: add nths
+- FunExt: axiom for functional extensionality
+- PropExt: axiom for propositional extensionality and related theorems
+- Prod: Cartesian product (extracted from Set)
+- Option: polymorphic option type
+- String: builtin string type
+- Tactic: tactic type for the eval tactic
+- Comp: isLe and isGe
+- List: mem_tail, nths and related properties
+- Bool: istrue=true
+
+### Changed
+
+- Set: moved Cartesian product to separate Prod file, pairing constructor renamed as "‚"
 
 ## 1.2.0 (2025-02-04)