From 0a9bb7a4c070a3d58ec487e704b13639df2af831 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sun, 25 Feb 2024 11:07:20 +0100
Subject: [PATCH] update README

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index dd8fa96..6043cac 100644
--- a/README.md
+++ b/README.md
@@ -31,7 +31,7 @@ opam install coq-hol-light
 **Usage in a Coq file**
 
 ```
-Require Import HOLLight.hol_upto_arith_opam.
+Require Import HOLLight.hol_light.
 Check thm_DIV_DIV.
 ```