From ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 16:06:14 +0200
Subject: Regenerate the test files and fix a proof

---
 tests/hol4/misc-constants/constantsTheory.sig | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'tests/hol4/misc-constants/constantsTheory.sig')

diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/misc-constants/constantsTheory.sig
index 149d7e22..287ad5f5 100644
--- a/tests/hol4/misc-constants/constantsTheory.sig
+++ b/tests/hol4/misc-constants/constantsTheory.sig
@@ -4,8 +4,6 @@ sig
   
   (*  Definitions  *)
     val add_fwd_def : thm
-    val core_num_u32_max_body_def : thm
-    val core_num_u32_max_c_def : thm
     val get_z1_fwd_def : thm
     val get_z1_z1_body_def : thm
     val get_z1_z1_c_def : thm
@@ -110,14 +108,6 @@ sig
       
       ⊢ ∀a b. add_fwd a b = i32_add a b
    
-   [core_num_u32_max_body_def]  Definition
-      
-      ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-   
-   [core_num_u32_max_c_def]  Definition
-      
-      ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-   
    [get_z1_fwd_def]  Definition
       
       ⊢ get_z1_fwd = Return get_z1_z1_c
@@ -321,7 +311,7 @@ sig
    
    [x1_body_def]  Definition
       
-      ⊢ x1_body = Return core_num_u32_max_c
+      ⊢ x1_body = Return core_u32_max
    
    [x1_c_def]  Definition
       
-- 
cgit v1.2.3