Update the HOL4 proofs for the last *release* version of HOL4

1 files changed, 54 insertions, 54 deletions

diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
index bea7eb76..a3e770ea 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
@@ -5,18 +5,18 @@ sig
   (*  Definitions  *)
     val hashmap_hash_map_t_TY_DEF : thm
     val hashmap_hash_map_t_case_def : thm
+    val hashmap_hash_map_t_hashmap_hash_map_max_load : thm
+    val hashmap_hash_map_t_hashmap_hash_map_max_load_factor : thm
+    val hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd : thm
+    val hashmap_hash_map_t_hashmap_hash_map_max_load_fupd : thm
+    val hashmap_hash_map_t_hashmap_hash_map_num_entries : thm
+    val hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd : thm
+    val hashmap_hash_map_t_hashmap_hash_map_slots : thm
+    val hashmap_hash_map_t_hashmap_hash_map_slots_fupd : thm
     val hashmap_hash_map_t_size_def : thm
     val hashmap_list_t_TY_DEF : thm
     val hashmap_list_t_case_def : thm
     val hashmap_list_t_size_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_fupd_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_fupd_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_fupd_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_fupd_def : thm
   
   (*  Theorems  *)
     val EXISTS_hashmap_hash_map_t : thm
@@ -73,92 +73,92 @@ sig
           hashmap_hash_map_t_CASE (hashmap_hash_map_t a0 a1 a2 a3) f =
           f a0 a1 a2 a3
    
-   [hashmap_hash_map_t_size_def]  Definition
-      
-      ⊢ ∀f a0 a1 a2 a3.
-          hashmap_hash_map_t_size f (hashmap_hash_map_t a0 a1 a2 a3) =
-          1 + pair_size (λv. 0) (λv. 0) a1
-   
-   [hashmap_list_t_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0'.
-                 ∀ $var$('hashmap_list_t').
-                   (∀a0'.
-                      (∃a0 a1 a2.
-                         a0' =
-                         (λa0 a1 a2.
-                              ind_type$CONSTR 0 (a0,a1)
-                                (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))
-                           a0 a1 a2 ∧ $var$('hashmap_list_t') a2) ∨
-                      a0' =
-                      ind_type$CONSTR (SUC 0) (ARB,ARB)
-                        (λn. ind_type$BOTTOM) ⇒
-                      $var$('hashmap_list_t') a0') ⇒
-                   $var$('hashmap_list_t') a0') rep
-   
-   [hashmap_list_t_case_def]  Definition
-      
-      ⊢ (∀a0 a1 a2 f v.
-           hashmap_list_t_CASE (HashmapListCons a0 a1 a2) f v = f a0 a1 a2) ∧
-        ∀f v. hashmap_list_t_CASE HashmapListNil f v = v
-   
-   [hashmap_list_t_size_def]  Definition
-      
-      ⊢ (∀f a0 a1 a2.
-           hashmap_list_t_size f (HashmapListCons a0 a1 a2) =
-           1 + (f a1 + hashmap_list_t_size f a2)) ∧
-        ∀f. hashmap_list_t_size f HashmapListNil = 0
-   
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_max_load]  Definition
       
       ⊢ ∀u p u0 v.
           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load = u0
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_max_load_factor]  Definition
       
       ⊢ ∀u p u0 v.
           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load_factor =
           p
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_fupd_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd]  Definition
       
       ⊢ ∀f u p u0 v.
           hashmap_hash_map_t u p u0 v with
           hashmap_hash_map_max_load_factor updated_by f =
           hashmap_hash_map_t u (f p) u0 v
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_fupd_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_max_load_fupd]  Definition
       
       ⊢ ∀f u p u0 v.
           hashmap_hash_map_t u p u0 v with
           hashmap_hash_map_max_load updated_by f =
           hashmap_hash_map_t u p (f u0) v
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_num_entries]  Definition
       
       ⊢ ∀u p u0 v.
           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_num_entries = u
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_fupd_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd]  Definition
       
       ⊢ ∀f u p u0 v.
           hashmap_hash_map_t u p u0 v with
           hashmap_hash_map_num_entries updated_by f =
           hashmap_hash_map_t (f u) p u0 v
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_slots]  Definition
       
       ⊢ ∀u p u0 v. (hashmap_hash_map_t u p u0 v).hashmap_hash_map_slots = v
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_fupd_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_slots_fupd]  Definition
       
       ⊢ ∀f u p u0 v.
           hashmap_hash_map_t u p u0 v with
           hashmap_hash_map_slots updated_by f =
           hashmap_hash_map_t u p u0 (f v)
    
+   [hashmap_hash_map_t_size_def]  Definition
+      
+      ⊢ ∀f a0 a1 a2 a3.
+          hashmap_hash_map_t_size f (hashmap_hash_map_t a0 a1 a2 a3) =
+          1 + pair_size (λv. 0) (λv. 0) a1
+   
+   [hashmap_list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('hashmap_list_t').
+                   (∀a0'.
+                      (∃a0 a1 a2.
+                         a0' =
+                         (λa0 a1 a2.
+                              ind_type$CONSTR 0 (a0,a1)
+                                (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))
+                           a0 a1 a2 ∧ $var$('hashmap_list_t') a2) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) (ARB,ARB)
+                        (λn. ind_type$BOTTOM) ⇒
+                      $var$('hashmap_list_t') a0') ⇒
+                   $var$('hashmap_list_t') a0') rep
+   
+   [hashmap_list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 a2 f v.
+           hashmap_list_t_CASE (HashmapListCons a0 a1 a2) f v = f a0 a1 a2) ∧
+        ∀f v. hashmap_list_t_CASE HashmapListNil f v = v
+   
+   [hashmap_list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1 a2.
+           hashmap_list_t_size f (HashmapListCons a0 a1 a2) =
+           1 + (f a1 + hashmap_list_t_size f a2)) ∧
+        ∀f. hashmap_list_t_size f HashmapListNil = 0
+   
    [EXISTS_hashmap_hash_map_t]  Theorem
       
       ⊢ ∀P. (∃h. P h) ⇔