update README

Deducteam · Jan 20, 2025 · f298390 · f298390
1 parent 7218723
commit f298390
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -3,6 +3,6 @@ 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/).
 
-## 1.0.0 (2025-01-13)
+## 1.0.0 (2025-01-20)
 
 First release.
diff --git a/README.md b/README.md
@@ -1,13 +1,13 @@
 HOL-Light definition of real numbers in Coq using N
 ---------------------------------------------------
 
-This library provides a translation in Coq of the definition of real numbers in HOL-Light, using the Coq type N for natural numbers.
+This library provides a translation in Coq of the definition of real numbers in HOL-Light, using the Coq type N for natural numbers (it is an adaptation of [coq-hol-light-real-with-nat](https://github.com/Deducteam/coq-hol-light-real-with-nat/)).
 
 It has been automatically generated from HOL-Light using [hol2dk](https://github.com/Deducteam/hol2dk) and [lambdapi](https://github.com/Deducteam/lambdapi).
 
 Proofs are not included but can be regenerated and rechecked by running [reproduce](https://github.com/Deducteam/coq-hol-light-real/blob/main/reproduce) (it takes about 7 minutes on a machine with 32 processors Intel Core i9-13950HX and 64 Gb RAM).
 
-As HOL-Light is based on higher-order logic, this library assumes classical logic, Hilbert's ε operator, functional and propositional extensionnality (see [HOLLight.v](https://github.com/Deducteam/coq-hol-light-real/blob/main/HOLLight.v) for more details):
+As HOL-Light is based on higher-order logic, this library assumes classical logic, Hilbert's ε operator, functional and propositional extensionnality:
 
 ```
 Axiom classic : forall P:Prop, P \/ ~ P.

diff --git a/coq-hol-light-real-with-N.opam b/coq-hol-light-real-with-N.opam
@@ -20,6 +20,6 @@ tags: [
   "keyword:HOL-Light"
   "category:Math/Arith/Misc"
   "category:Math/Arith/Real numbers"
-  "date:2024-11-03"
+  "date:2025-01-20"
   "logpath:HOLLight_Real_With_N"
 ]