From b1dd8274d7a1cff2b9427e4356b66c4e63fe498c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 15 May 2023 16:48:52 +0200
Subject: Make a minor modification

---
 backends/hol4/divDefLib.sig | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig
index 0de88db5..ac9c6892 100644
--- a/backends/hol4/divDefLib.sig
+++ b/backends/hol4/divDefLib.sig
@@ -16,9 +16,11 @@
    by the fixed point upon defining ‘explore_tree’ and ‘explore_node’:
 
    {[
-     Datatype tree:
-     | Leaf : int
-     | Node : tree list
+     Datatype:
+       tree =
+         Leaf int
+       | Node (tree list)
+     End
 
      explore_tree (t : tree) : tree =
        case t of
-- 
cgit v1.2.3