summaryrefslogtreecommitdiff
path: root/tests/hol4
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hol4/betree/betreeMain_OpaqueScript.sml26
-rw-r--r--tests/hol4/betree/betreeMain_OpaqueTheory.sig11
-rw-r--r--tests/hol4/betree/betree_FunsScript.sml (renamed from tests/hol4/betree/betreeMain_FunsScript.sml)120
-rw-r--r--tests/hol4/betree/betree_FunsTheory.sig (renamed from tests/hol4/betree/betreeMain_FunsTheory.sig)6
-rw-r--r--tests/hol4/betree/betree_OpaqueScript.sml26
-rw-r--r--tests/hol4/betree/betree_OpaqueTheory.sig11
-rw-r--r--tests/hol4/betree/betree_TypesScript.sml (renamed from tests/hol4/betree/betreeMain_TypesScript.sml)22
-rw-r--r--tests/hol4/betree/betree_TypesTheory.sig (renamed from tests/hol4/betree/betreeMain_TypesTheory.sig)6
-rw-r--r--tests/hol4/constants/Holmakefile (renamed from tests/hol4/hashmap_on_disk/Holmakefile)0
-rw-r--r--tests/hol4/constants/constantsScript.sml (renamed from tests/hol4/misc-constants/constantsScript.sml)0
-rw-r--r--tests/hol4/constants/constantsTheory.sig (renamed from tests/hol4/misc-constants/constantsTheory.sig)0
-rw-r--r--tests/hol4/external/Holmakefile (renamed from tests/hol4/misc-constants/Holmakefile)0
-rw-r--r--tests/hol4/external/external_FunsScript.sml (renamed from tests/hol4/misc-external/external_FunsScript.sml)0
-rw-r--r--tests/hol4/external/external_FunsTheory.sig (renamed from tests/hol4/misc-external/external_FunsTheory.sig)0
-rw-r--r--tests/hol4/external/external_OpaqueScript.sml (renamed from tests/hol4/misc-external/external_OpaqueScript.sml)0
-rw-r--r--tests/hol4/external/external_OpaqueTheory.sig (renamed from tests/hol4/misc-external/external_OpaqueTheory.sig)0
-rw-r--r--tests/hol4/external/external_TypesScript.sml (renamed from tests/hol4/misc-external/external_TypesScript.sml)0
-rw-r--r--tests/hol4/external/external_TypesTheory.sig (renamed from tests/hol4/misc-external/external_TypesTheory.sig)0
-rw-r--r--tests/hol4/hashmap_main/Holmakefile (renamed from tests/hol4/misc-external/Holmakefile)0
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_FunsScript.sml (renamed from tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml)4
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig (renamed from tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig)4
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml (renamed from tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml)4
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig (renamed from tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig)0
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_TypesScript.sml (renamed from tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml)0
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig (renamed from tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig)0
-rw-r--r--tests/hol4/loops/Holmakefile (renamed from tests/hol4/misc-loops/Holmakefile)0
-rw-r--r--tests/hol4/loops/loops_FunsScript.sml (renamed from tests/hol4/misc-loops/loops_FunsScript.sml)0
-rw-r--r--tests/hol4/loops/loops_FunsTheory.sig (renamed from tests/hol4/misc-loops/loops_FunsTheory.sig)0
-rw-r--r--tests/hol4/loops/loops_TypesScript.sml (renamed from tests/hol4/misc-loops/loops_TypesScript.sml)0
-rw-r--r--tests/hol4/loops/loops_TypesTheory.sig (renamed from tests/hol4/misc-loops/loops_TypesTheory.sig)0
-rw-r--r--tests/hol4/no_nested_borrows/Holmakefile (renamed from tests/hol4/misc-no_nested_borrows/Holmakefile)0
-rw-r--r--tests/hol4/no_nested_borrows/noNestedBorrowsScript.sml (renamed from tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml)0
-rw-r--r--tests/hol4/no_nested_borrows/noNestedBorrowsTheory.sig (renamed from tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig)0
-rw-r--r--tests/hol4/paper/Holmakefile (renamed from tests/hol4/misc-paper/Holmakefile)0
-rw-r--r--tests/hol4/paper/paperScript.sml (renamed from tests/hol4/misc-paper/paperScript.sml)0
-rw-r--r--tests/hol4/paper/paperTheory.sig (renamed from tests/hol4/misc-paper/paperTheory.sig)0
-rw-r--r--tests/hol4/polonius_list/Holmakefile (renamed from tests/hol4/misc-polonius_list/Holmakefile)0
-rw-r--r--tests/hol4/polonius_list/poloniusListScript.sml (renamed from tests/hol4/misc-polonius_list/poloniusListScript.sml)0
-rw-r--r--tests/hol4/polonius_list/poloniusListTheory.sig (renamed from tests/hol4/misc-polonius_list/poloniusListTheory.sig)0
39 files changed, 120 insertions, 120 deletions
diff --git a/tests/hol4/betree/betreeMain_OpaqueScript.sml b/tests/hol4/betree/betreeMain_OpaqueScript.sml
deleted file mode 100644
index 1d16db4c..00000000
--- a/tests/hol4/betree/betreeMain_OpaqueScript.sml
+++ /dev/null
@@ -1,26 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external function declarations *)
-open primitivesLib divDefLib
-open betreeMain_TypesTheory
-
-val _ = new_theory "betreeMain_Opaque"
-
-
-(** [betree_main::betree_utils::load_internal_node]: forward function *)val _ = new_constant ("betree_utils_load_internal_node_fwd",
- “:u64 -> state -> (state # (u64 # betree_message_t) betree_list_t)
- result”)
-
-(** [betree_main::betree_utils::store_internal_node]: forward function *)val _ = new_constant ("betree_utils_store_internal_node_fwd",
- “:u64 -> (u64 # betree_message_t) betree_list_t -> state -> (state # unit)
- result”)
-
-(** [betree_main::betree_utils::load_leaf_node]: forward function *)val _ = new_constant ("betree_utils_load_leaf_node_fwd",
- “:u64 -> state -> (state # (u64 # u64) betree_list_t) result”)
-
-(** [betree_main::betree_utils::store_leaf_node]: forward function *)val _ = new_constant ("betree_utils_store_leaf_node_fwd",
- “:u64 -> (u64 # u64) betree_list_t -> state -> (state # unit) result”)
-
-(** [core::option::Option::{0}::unwrap]: forward function *)val _ = new_constant ("core_option_option_unwrap_fwd",
- “:'t option -> state -> (state # 't) result”)
-
-val _ = export_theory ()
diff --git a/tests/hol4/betree/betreeMain_OpaqueTheory.sig b/tests/hol4/betree/betreeMain_OpaqueTheory.sig
deleted file mode 100644
index da7559a0..00000000
--- a/tests/hol4/betree/betreeMain_OpaqueTheory.sig
+++ /dev/null
@@ -1,11 +0,0 @@
-signature betreeMain_OpaqueTheory =
-sig
- type thm = Thm.thm
-
- val betreeMain_Opaque_grammars : type_grammar.grammar * term_grammar.grammar
-(*
- [betreeMain_Types] Parent theory of "betreeMain_Opaque"
-
-
-*)
-end
diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betree_FunsScript.sml
index bd16c16c..49bcb446 100644
--- a/tests/hol4/betree/betreeMain_FunsScript.sml
+++ b/tests/hol4/betree/betree_FunsScript.sml
@@ -1,13 +1,13 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: function definitions *)
+(** [betree]: function definitions *)
open primitivesLib divDefLib
-open betreeMain_TypesTheory betreeMain_OpaqueTheory
+open betree_TypesTheory betree_OpaqueTheory
-val _ = new_theory "betreeMain_Funs"
+val _ = new_theory "betree_Funs"
val betree_load_internal_node_fwd_def = Define ‘
- (** [betree_main::betree::load_internal_node]: forward function *)
+ (** [betree::betree::load_internal_node]: forward function *)
betree_load_internal_node_fwd
(id : u64) (st : state) :
(state # (u64 # betree_message_t) betree_list_t) result
@@ -16,7 +16,7 @@ val betree_load_internal_node_fwd_def = Define ‘
val betree_store_internal_node_fwd_def = Define ‘
- (** [betree_main::betree::store_internal_node]: forward function *)
+ (** [betree::betree::store_internal_node]: forward function *)
betree_store_internal_node_fwd
(id : u64) (content : (u64 # betree_message_t) betree_list_t) (st : state)
:
@@ -29,14 +29,14 @@ val betree_store_internal_node_fwd_def = Define ‘
val betree_load_leaf_node_fwd_def = Define ‘
- (** [betree_main::betree::load_leaf_node]: forward function *)
+ (** [betree::betree::load_leaf_node]: forward function *)
betree_load_leaf_node_fwd
(id : u64) (st : state) : (state # (u64 # u64) betree_list_t) result =
betree_utils_load_leaf_node_fwd id st
val betree_store_leaf_node_fwd_def = Define ‘
- (** [betree_main::betree::store_leaf_node]: forward function *)
+ (** [betree::betree::store_leaf_node]: forward function *)
betree_store_leaf_node_fwd
(id : u64) (content : (u64 # u64) betree_list_t) (st : state) :
(state # unit) result
@@ -48,7 +48,7 @@ val betree_store_leaf_node_fwd_def = Define ‘
val betree_fresh_node_id_fwd_def = Define ‘
- (** [betree_main::betree::fresh_node_id]: forward function *)
+ (** [betree::betree::fresh_node_id]: forward function *)
betree_fresh_node_id_fwd (counter : u64) : u64 result =
do
_ <- u64_add counter (int_to_u64 1);
@@ -57,19 +57,19 @@ val betree_fresh_node_id_fwd_def = Define ‘
val betree_fresh_node_id_back_def = Define ‘
- (** [betree_main::betree::fresh_node_id]: backward function 0 *)
+ (** [betree::betree::fresh_node_id]: backward function 0 *)
betree_fresh_node_id_back (counter : u64) : u64 result =
u64_add counter (int_to_u64 1)
val betree_node_id_counter_new_fwd_def = Define ‘
- (** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *)
+ (** [betree::betree::NodeIdCounter::{0}::new]: forward function *)
betree_node_id_counter_new_fwd : betree_node_id_counter_t result =
Return (<| betree_node_id_counter_next_node_id := (int_to_u64 0) |>)
val betree_node_id_counter_fresh_id_fwd_def = Define ‘
- (** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *)
+ (** [betree::betree::NodeIdCounter::{0}::fresh_id]: forward function *)
betree_node_id_counter_fresh_id_fwd
(self : betree_node_id_counter_t) : u64 result =
do
@@ -79,7 +79,7 @@ val betree_node_id_counter_fresh_id_fwd_def = Define ‘
val betree_node_id_counter_fresh_id_back_def = Define ‘
- (** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
+ (** [betree::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
betree_node_id_counter_fresh_id_back
(self : betree_node_id_counter_t) : betree_node_id_counter_t result =
do
@@ -89,7 +89,7 @@ val betree_node_id_counter_fresh_id_back_def = Define ‘
val betree_upsert_update_fwd_def = Define ‘
- (** [betree_main::betree::upsert_update]: forward function *)
+ (** [betree::betree::upsert_update]: forward function *)
betree_upsert_update_fwd
(prev : u64 option) (st : betree_upsert_fun_state_t) : u64 result =
(case prev of
@@ -109,7 +109,7 @@ val betree_upsert_update_fwd_def = Define ‘
val [betree_list_len_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::List::{1}::len]: forward function *)
+ (** [betree::betree::List::{1}::len]: forward function *)
betree_list_len_fwd (self : 't betree_list_t) : u64 result =
(case self of
| BetreeListCons t tl =>
@@ -121,7 +121,7 @@ val [betree_list_len_fwd_def] = DefineDiv ‘
val [betree_list_split_at_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::List::{1}::split_at]: forward function *)
+ (** [betree::betree::List::{1}::split_at]: forward function *)
betree_list_split_at_fwd
(self : 't betree_list_t) (n : u64) :
('t betree_list_t # 't betree_list_t) result
@@ -140,7 +140,7 @@ val [betree_list_split_at_fwd_def] = DefineDiv ‘
val betree_list_push_front_fwd_back_def = Define ‘
- (** [betree_main::betree::List::{1}::push_front]: merged forward/backward function
+ (** [betree::betree::List::{1}::push_front]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
betree_list_push_front_fwd_back
(self : 't betree_list_t) (x : 't) : 't betree_list_t result =
@@ -150,7 +150,7 @@ val betree_list_push_front_fwd_back_def = Define ‘
val betree_list_pop_front_fwd_def = Define ‘
- (** [betree_main::betree::List::{1}::pop_front]: forward function *)
+ (** [betree::betree::List::{1}::pop_front]: forward function *)
betree_list_pop_front_fwd (self : 't betree_list_t) : 't result =
let ls = mem_replace_fwd self BetreeListNil in
(case ls of
@@ -159,7 +159,7 @@ val betree_list_pop_front_fwd_def = Define ‘
val betree_list_pop_front_back_def = Define ‘
- (** [betree_main::betree::List::{1}::pop_front]: backward function 0 *)
+ (** [betree::betree::List::{1}::pop_front]: backward function 0 *)
betree_list_pop_front_back
(self : 't betree_list_t) : 't betree_list_t result =
let ls = mem_replace_fwd self BetreeListNil in
@@ -169,7 +169,7 @@ val betree_list_pop_front_back_def = Define ‘
val betree_list_hd_fwd_def = Define ‘
- (** [betree_main::betree::List::{1}::hd]: forward function *)
+ (** [betree::betree::List::{1}::hd]: forward function *)
betree_list_hd_fwd (self : 't betree_list_t) : 't result =
(case self of
| BetreeListCons hd l => Return hd
@@ -177,7 +177,7 @@ val betree_list_hd_fwd_def = Define ‘
val betree_list_head_has_key_fwd_def = Define ‘
- (** [betree_main::betree::List::{2}::head_has_key]: forward function *)
+ (** [betree::betree::List::{2}::head_has_key]: forward function *)
betree_list_head_has_key_fwd
(self : (u64 # 't) betree_list_t) (key : u64) : bool result =
(case self of
@@ -186,7 +186,7 @@ val betree_list_head_has_key_fwd_def = Define ‘
val [betree_list_partition_at_pivot_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *)
+ (** [betree::betree::List::{2}::partition_at_pivot]: forward function *)
betree_list_partition_at_pivot_fwd
(self : (u64 # 't) betree_list_t) (pivot : u64) :
((u64 # 't) betree_list_t # (u64 # 't) betree_list_t) result
@@ -207,7 +207,7 @@ val [betree_list_partition_at_pivot_fwd_def] = DefineDiv ‘
val betree_leaf_split_fwd_def = Define ‘
- (** [betree_main::betree::Leaf::{3}::split]: forward function *)
+ (** [betree::betree::Leaf::{3}::split]: forward function *)
betree_leaf_split_fwd
(self : betree_leaf_t) (content : (u64 # u64) betree_list_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
@@ -249,7 +249,7 @@ val betree_leaf_split_fwd_def = Define ‘
val betree_leaf_split_back_def = Define ‘
- (** [betree_main::betree::Leaf::{3}::split]: backward function 2 *)
+ (** [betree::betree::Leaf::{3}::split]: backward function 2 *)
betree_leaf_split_back
(self : betree_leaf_t) (content : (u64 # u64) betree_list_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
@@ -272,7 +272,7 @@ val betree_leaf_split_back_def = Define ‘
val [betree_node_lookup_first_message_for_key_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
+ (** [betree::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
betree_node_lookup_first_message_for_key_fwd
(key : u64) (msgs : (u64 # betree_message_t) betree_list_t) :
(u64 # betree_message_t) betree_list_t result
@@ -287,7 +287,7 @@ val [betree_node_lookup_first_message_for_key_fwd_def] = DefineDiv ‘
val [betree_node_lookup_first_message_for_key_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *)
+ (** [betree::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *)
betree_node_lookup_first_message_for_key_back
(key : u64) (msgs : (u64 # betree_message_t) betree_list_t)
(ret : (u64 # betree_message_t) betree_list_t) :
@@ -308,7 +308,7 @@ val [betree_node_lookup_first_message_for_key_back_def] = DefineDiv ‘
val [betree_node_apply_upserts_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::apply_upserts]: forward function *)
+ (** [betree::betree::Node::{5}::apply_upserts]: forward function *)
betree_node_apply_upserts_fwd
(msgs : (u64 # betree_message_t) betree_list_t) (prev : u64 option)
(key : u64) (st : state) :
@@ -341,7 +341,7 @@ val [betree_node_apply_upserts_fwd_def] = DefineDiv ‘
val [betree_node_apply_upserts_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *)
+ (** [betree::betree::Node::{5}::apply_upserts]: backward function 0 *)
betree_node_apply_upserts_back
(msgs : (u64 # betree_message_t) betree_list_t) (prev : u64 option)
(key : u64) (st : state) :
@@ -373,7 +373,7 @@ val [betree_node_apply_upserts_back_def] = DefineDiv ‘
val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+ (** [betree::betree::Node::{5}::lookup_in_bindings]: forward function *)
betree_node_lookup_in_bindings_fwd
(key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result =
(case bindings of
@@ -389,7 +389,7 @@ val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘
val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def, betree_node_lookup_fwd_def, betree_node_lookup_back_def] = DefineDiv ‘
- (** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+ (** [betree::betree::Internal::{4}::lookup_in_children]: forward function *)
(betree_internal_lookup_in_children_fwd
(self : betree_internal_t) (key : u64) (st : state) :
(state # u64 option) result
@@ -399,7 +399,7 @@ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_child
else betree_node_lookup_fwd self.betree_internal_right key st)
/\
- (** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+ (** [betree::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
(betree_internal_lookup_in_children_back
(self : betree_internal_t) (key : u64) (st : state) :
betree_internal_t result
@@ -417,7 +417,7 @@ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_child
od))
/\
- (** [betree_main::betree::Node::{5}::lookup]: forward function *)
+ (** [betree::betree::Node::{5}::lookup]: forward function *)
(betree_node_lookup_fwd
(self : betree_node_t) (key : u64) (st : state) :
(state # u64 option) result
@@ -487,7 +487,7 @@ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_child
od))
/\
- (** [betree_main::betree::Node::{5}::lookup]: backward function 0 *)
+ (** [betree::betree::Node::{5}::lookup]: backward function 0 *)
betree_node_lookup_back
(self : betree_node_t) (key : u64) (st : state) : betree_node_t result =
(case self of
@@ -556,7 +556,7 @@ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_child
val [betree_node_filter_messages_for_key_fwd_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
+ (** [betree::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
betree_node_filter_messages_for_key_fwd_back
(key : u64) (msgs : (u64 # betree_message_t) betree_list_t) :
@@ -576,7 +576,7 @@ val [betree_node_filter_messages_for_key_fwd_back_def] = DefineDiv ‘
val [betree_node_lookup_first_message_after_key_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *)
+ (** [betree::betree::Node::{5}::lookup_first_message_after_key]: forward function *)
betree_node_lookup_first_message_after_key_fwd
(key : u64) (msgs : (u64 # betree_message_t) betree_list_t) :
(u64 # betree_message_t) betree_list_t result
@@ -591,7 +591,7 @@ val [betree_node_lookup_first_message_after_key_fwd_def] = DefineDiv ‘
val [betree_node_lookup_first_message_after_key_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *)
+ (** [betree::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *)
betree_node_lookup_first_message_after_key_back
(key : u64) (msgs : (u64 # betree_message_t) betree_list_t)
(ret : (u64 # betree_message_t) betree_list_t) :
@@ -612,7 +612,7 @@ val [betree_node_lookup_first_message_after_key_back_def] = DefineDiv ‘
val betree_node_apply_to_internal_fwd_back_def = Define ‘
- (** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function
+ (** [betree::betree::Node::{5}::apply_to_internal]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
betree_node_apply_to_internal_fwd_back
(msgs : (u64 # betree_message_t) betree_list_t) (key : u64)
@@ -679,7 +679,7 @@ val betree_node_apply_to_internal_fwd_back_def = Define ‘
val [betree_node_apply_messages_to_internal_fwd_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function
+ (** [betree::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
betree_node_apply_messages_to_internal_fwd_back
(msgs : (u64 # betree_message_t) betree_list_t)
@@ -697,7 +697,7 @@ val [betree_node_apply_messages_to_internal_fwd_back_def] = DefineDiv ‘
val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+ (** [betree::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
betree_node_lookup_mut_in_bindings_fwd
(key : u64) (bindings : (u64 # u64) betree_list_t) :
(u64 # u64) betree_list_t result
@@ -712,7 +712,7 @@ val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘
val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+ (** [betree::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
betree_node_lookup_mut_in_bindings_back
(key : u64) (bindings : (u64 # u64) betree_list_t)
(ret : (u64 # u64) betree_list_t) :
@@ -732,7 +732,7 @@ val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘
val betree_node_apply_to_leaf_fwd_back_def = Define ‘
- (** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+ (** [betree::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
betree_node_apply_to_leaf_fwd_back
(bindings : (u64 # u64) betree_list_t) (key : u64)
@@ -786,7 +786,7 @@ val betree_node_apply_to_leaf_fwd_back_def = Define ‘
val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘
- (** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+ (** [betree::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
betree_node_apply_messages_to_leaf_fwd_back
(bindings : (u64 # u64) betree_list_t)
@@ -804,7 +804,7 @@ val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘
val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def] = DefineDiv ‘
- (** [betree_main::betree::Internal::{4}::flush]: forward function *)
+ (** [betree::betree::Internal::{4}::flush]: forward function *)
(betree_internal_flush_fwd
(self : betree_internal_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t)
@@ -853,7 +853,7 @@ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_
od)
/\
- (** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+ (** [betree::betree::Internal::{4}::flush]: backward function 0 *)
(betree_internal_flush_back
(self : betree_internal_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t)
@@ -901,7 +901,7 @@ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_
od)
/\
- (** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
+ (** [betree::betree::Node::{5}::apply_messages]: forward function *)
(betree_node_apply_messages_fwd
(self : betree_node_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t)
@@ -956,7 +956,7 @@ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_
od))
/\
- (** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
+ (** [betree::betree::Node::{5}::apply_messages]: backward function 0 *)
betree_node_apply_messages_back
(self : betree_node_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t)
@@ -1014,7 +1014,7 @@ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_
val betree_node_apply_fwd_def = Define ‘
- (** [betree_main::betree::Node::{5}::apply]: forward function *)
+ (** [betree::betree::Node::{5}::apply]: forward function *)
betree_node_apply_fwd
(self : betree_node_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t) (key : u64)
@@ -1034,7 +1034,7 @@ val betree_node_apply_fwd_def = Define ‘
val betree_node_apply_back_def = Define ‘
- (** [betree_main::betree::Node::{5}::apply]: backward function 0 *)
+ (** [betree::betree::Node::{5}::apply]: backward function 0 *)
betree_node_apply_back
(self : betree_node_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t) (key : u64)
@@ -1047,7 +1047,7 @@ val betree_node_apply_back_def = Define ‘
val betree_be_tree_new_fwd_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::new]: forward function *)
+ (** [betree::betree::BeTree::{6}::new]: forward function *)
betree_be_tree_new_fwd
(min_flush_size : u64) (split_size : u64) (st : state) :
(state # betree_be_tree_t) result
@@ -1073,7 +1073,7 @@ val betree_be_tree_new_fwd_def = Define ‘
val betree_be_tree_apply_fwd_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::apply]: forward function *)
+ (** [betree::betree::BeTree::{6}::apply]: forward function *)
betree_be_tree_apply_fwd
(self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state)
:
@@ -1091,7 +1091,7 @@ val betree_be_tree_apply_fwd_def = Define ‘
val betree_be_tree_apply_back_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *)
+ (** [betree::betree::BeTree::{6}::apply]: backward function 0 *)
betree_be_tree_apply_back
(self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state)
:
@@ -1111,7 +1111,7 @@ val betree_be_tree_apply_back_def = Define ‘
val betree_be_tree_insert_fwd_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::insert]: forward function *)
+ (** [betree::betree::BeTree::{6}::insert]: forward function *)
betree_be_tree_insert_fwd
(self : betree_be_tree_t) (key : u64) (value : u64) (st : state) :
(state # unit) result
@@ -1125,7 +1125,7 @@ val betree_be_tree_insert_fwd_def = Define ‘
val betree_be_tree_insert_back_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *)
+ (** [betree::betree::BeTree::{6}::insert]: backward function 0 *)
betree_be_tree_insert_back
(self : betree_be_tree_t) (key : u64) (value : u64) (st : state) :
betree_be_tree_t result
@@ -1134,7 +1134,7 @@ val betree_be_tree_insert_back_def = Define ‘
val betree_be_tree_delete_fwd_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::delete]: forward function *)
+ (** [betree::betree::BeTree::{6}::delete]: forward function *)
betree_be_tree_delete_fwd
(self : betree_be_tree_t) (key : u64) (st : state) :
(state # unit) result
@@ -1147,7 +1147,7 @@ val betree_be_tree_delete_fwd_def = Define ‘
val betree_be_tree_delete_back_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *)
+ (** [betree::betree::BeTree::{6}::delete]: backward function 0 *)
betree_be_tree_delete_back
(self : betree_be_tree_t) (key : u64) (st : state) :
betree_be_tree_t result
@@ -1156,7 +1156,7 @@ val betree_be_tree_delete_back_def = Define ‘
val betree_be_tree_upsert_fwd_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::upsert]: forward function *)
+ (** [betree::betree::BeTree::{6}::upsert]: forward function *)
betree_be_tree_upsert_fwd
(self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t)
(st : state) :
@@ -1170,7 +1170,7 @@ val betree_be_tree_upsert_fwd_def = Define ‘
val betree_be_tree_upsert_back_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *)
+ (** [betree::betree::BeTree::{6}::upsert]: backward function 0 *)
betree_be_tree_upsert_back
(self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t)
(st : state) :
@@ -1180,7 +1180,7 @@ val betree_be_tree_upsert_back_def = Define ‘
val betree_be_tree_lookup_fwd_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::lookup]: forward function *)
+ (** [betree::betree::BeTree::{6}::lookup]: forward function *)
betree_be_tree_lookup_fwd
(self : betree_be_tree_t) (key : u64) (st : state) :
(state # u64 option) result
@@ -1189,7 +1189,7 @@ val betree_be_tree_lookup_fwd_def = Define ‘
val betree_be_tree_lookup_back_def = Define ‘
- (** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *)
+ (** [betree::betree::BeTree::{6}::lookup]: backward function 0 *)
betree_be_tree_lookup_back
(self : betree_be_tree_t) (key : u64) (st : state) :
betree_be_tree_t result
@@ -1201,12 +1201,12 @@ val betree_be_tree_lookup_back_def = Define ‘
val main_fwd_def = Define ‘
- (** [betree_main::main]: forward function *)
+ (** [betree::main]: forward function *)
main_fwd : unit result =
Return ()
-(** Unit test for [betree_main::main] *)
+(** Unit test for [betree::main] *)
val _ = assert_return (“main_fwd”)
val _ = export_theory ()
diff --git a/tests/hol4/betree/betreeMain_FunsTheory.sig b/tests/hol4/betree/betree_FunsTheory.sig
index c922ca9f..4127cba1 100644
--- a/tests/hol4/betree/betreeMain_FunsTheory.sig
+++ b/tests/hol4/betree/betree_FunsTheory.sig
@@ -1,4 +1,4 @@
-signature betreeMain_FunsTheory =
+signature betree_FunsTheory =
sig
type thm = Thm.thm
@@ -60,9 +60,9 @@ sig
val betree_upsert_update_fwd_def : thm
val main_fwd_def : thm
- val betreeMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar
+ val betree_Funs_grammars : type_grammar.grammar * term_grammar.grammar
(*
- [betreeMain_Opaque] Parent theory of "betreeMain_Funs"
+ [betree_Opaque] Parent theory of "betree_Funs"
[betree_be_tree_apply_back_def] Definition
diff --git a/tests/hol4/betree/betree_OpaqueScript.sml b/tests/hol4/betree/betree_OpaqueScript.sml
new file mode 100644
index 00000000..d8fdf6b5
--- /dev/null
+++ b/tests/hol4/betree/betree_OpaqueScript.sml
@@ -0,0 +1,26 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree]: external function declarations *)
+open primitivesLib divDefLib
+open betree_TypesTheory
+
+val _ = new_theory "betree_Opaque"
+
+
+(** [betree::betree_utils::load_internal_node]: forward function *)val _ = new_constant ("betree_utils_load_internal_node_fwd",
+ “:u64 -> state -> (state # (u64 # betree_message_t) betree_list_t)
+ result”)
+
+(** [betree::betree_utils::store_internal_node]: forward function *)val _ = new_constant ("betree_utils_store_internal_node_fwd",
+ “:u64 -> (u64 # betree_message_t) betree_list_t -> state -> (state # unit)
+ result”)
+
+(** [betree::betree_utils::load_leaf_node]: forward function *)val _ = new_constant ("betree_utils_load_leaf_node_fwd",
+ “:u64 -> state -> (state # (u64 # u64) betree_list_t) result”)
+
+(** [betree::betree_utils::store_leaf_node]: forward function *)val _ = new_constant ("betree_utils_store_leaf_node_fwd",
+ “:u64 -> (u64 # u64) betree_list_t -> state -> (state # unit) result”)
+
+(** [core::option::Option::{0}::unwrap]: forward function *)val _ = new_constant ("core_option_option_unwrap_fwd",
+ “:'t option -> state -> (state # 't) result”)
+
+val _ = export_theory ()
diff --git a/tests/hol4/betree/betree_OpaqueTheory.sig b/tests/hol4/betree/betree_OpaqueTheory.sig
new file mode 100644
index 00000000..9452ff0f
--- /dev/null
+++ b/tests/hol4/betree/betree_OpaqueTheory.sig
@@ -0,0 +1,11 @@
+signature betree_OpaqueTheory =
+sig
+ type thm = Thm.thm
+
+ val betree_Opaque_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [betree_Types] Parent theory of "betree_Opaque"
+
+
+*)
+end
diff --git a/tests/hol4/betree/betreeMain_TypesScript.sml b/tests/hol4/betree/betree_TypesScript.sml
index 779f6abb..93be2f46 100644
--- a/tests/hol4/betree/betreeMain_TypesScript.sml
+++ b/tests/hol4/betree/betree_TypesScript.sml
@@ -1,24 +1,24 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
+(** [betree]: type definitions *)
open primitivesLib divDefLib
-val _ = new_theory "betreeMain_Types"
+val _ = new_theory "betree_Types"
Datatype:
- (** [betree_main::betree::List] *)
+ (** [betree::betree::List] *)
betree_list_t = | BetreeListCons 't betree_list_t | BetreeListNil
End
Datatype:
- (** [betree_main::betree::UpsertFunState] *)
+ (** [betree::betree::UpsertFunState] *)
betree_upsert_fun_state_t =
| BetreeUpsertFunStateAdd u64
| BetreeUpsertFunStateSub u64
End
Datatype:
- (** [betree_main::betree::Message] *)
+ (** [betree::betree::Message] *)
betree_message_t =
| BetreeMessageInsert u64
| BetreeMessageDelete
@@ -26,12 +26,12 @@ Datatype:
End
Datatype:
- (** [betree_main::betree::Leaf] *)
+ (** [betree::betree::Leaf] *)
betree_leaf_t = <| betree_leaf_id : u64; betree_leaf_size : u64; |>
End
Datatype:
- (** [betree_main::betree::Internal] *)
+ (** [betree::betree::Internal] *)
betree_internal_t =
<|
betree_internal_id : u64;
@@ -41,14 +41,14 @@ Datatype:
|>
;
- (** [betree_main::betree::Node] *)
+ (** [betree::betree::Node] *)
betree_node_t =
| BetreeNodeInternal betree_internal_t
| BetreeNodeLeaf betree_leaf_t
End
Datatype:
- (** [betree_main::betree::Params] *)
+ (** [betree::betree::Params] *)
betree_params_t =
<|
betree_params_min_flush_size : u64; betree_params_split_size : u64;
@@ -56,12 +56,12 @@ Datatype:
End
Datatype:
- (** [betree_main::betree::NodeIdCounter] *)
+ (** [betree::betree::NodeIdCounter] *)
betree_node_id_counter_t = <| betree_node_id_counter_next_node_id : u64; |>
End
Datatype:
- (** [betree_main::betree::BeTree] *)
+ (** [betree::betree::BeTree] *)
betree_be_tree_t =
<|
betree_be_tree_params : betree_params_t;
diff --git a/tests/hol4/betree/betreeMain_TypesTheory.sig b/tests/hol4/betree/betree_TypesTheory.sig
index cffe6afb..ee2ec4b5 100644
--- a/tests/hol4/betree/betreeMain_TypesTheory.sig
+++ b/tests/hol4/betree/betree_TypesTheory.sig
@@ -1,4 +1,4 @@
-signature betreeMain_TypesTheory =
+signature betree_TypesTheory =
sig
type thm = Thm.thm
@@ -185,9 +185,9 @@ sig
val datatype_betree_params_t : thm
val datatype_betree_upsert_fun_state_t : thm
- val betreeMain_Types_grammars : type_grammar.grammar * term_grammar.grammar
+ val betree_Types_grammars : type_grammar.grammar * term_grammar.grammar
(*
- [divDef] Parent theory of "betreeMain_Types"
+ [divDef] Parent theory of "betree_Types"
[betree_be_tree_t_TY_DEF] Definition
diff --git a/tests/hol4/hashmap_on_disk/Holmakefile b/tests/hol4/constants/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/hashmap_on_disk/Holmakefile
+++ b/tests/hol4/constants/Holmakefile
diff --git a/tests/hol4/misc-constants/constantsScript.sml b/tests/hol4/constants/constantsScript.sml
index 40a319c6..40a319c6 100644
--- a/tests/hol4/misc-constants/constantsScript.sml
+++ b/tests/hol4/constants/constantsScript.sml
diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/constants/constantsTheory.sig
index 287ad5f5..287ad5f5 100644
--- a/tests/hol4/misc-constants/constantsTheory.sig
+++ b/tests/hol4/constants/constantsTheory.sig
diff --git a/tests/hol4/misc-constants/Holmakefile b/tests/hol4/external/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-constants/Holmakefile
+++ b/tests/hol4/external/Holmakefile
diff --git a/tests/hol4/misc-external/external_FunsScript.sml b/tests/hol4/external/external_FunsScript.sml
index f3692ee2..f3692ee2 100644
--- a/tests/hol4/misc-external/external_FunsScript.sml
+++ b/tests/hol4/external/external_FunsScript.sml
diff --git a/tests/hol4/misc-external/external_FunsTheory.sig b/tests/hol4/external/external_FunsTheory.sig
index 490f9d06..490f9d06 100644
--- a/tests/hol4/misc-external/external_FunsTheory.sig
+++ b/tests/hol4/external/external_FunsTheory.sig
diff --git a/tests/hol4/misc-external/external_OpaqueScript.sml b/tests/hol4/external/external_OpaqueScript.sml
index b5a6d91d..b5a6d91d 100644
--- a/tests/hol4/misc-external/external_OpaqueScript.sml
+++ b/tests/hol4/external/external_OpaqueScript.sml
diff --git a/tests/hol4/misc-external/external_OpaqueTheory.sig b/tests/hol4/external/external_OpaqueTheory.sig
index 7cd7a08c..7cd7a08c 100644
--- a/tests/hol4/misc-external/external_OpaqueTheory.sig
+++ b/tests/hol4/external/external_OpaqueTheory.sig
diff --git a/tests/hol4/misc-external/external_TypesScript.sml b/tests/hol4/external/external_TypesScript.sml
index d290c3f6..d290c3f6 100644
--- a/tests/hol4/misc-external/external_TypesScript.sml
+++ b/tests/hol4/external/external_TypesScript.sml
diff --git a/tests/hol4/misc-external/external_TypesTheory.sig b/tests/hol4/external/external_TypesTheory.sig
index 17e2e8e3..17e2e8e3 100644
--- a/tests/hol4/misc-external/external_TypesTheory.sig
+++ b/tests/hol4/external/external_TypesTheory.sig
diff --git a/tests/hol4/misc-external/Holmakefile b/tests/hol4/hashmap_main/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-external/Holmakefile
+++ b/tests/hol4/hashmap_main/Holmakefile
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
index c1e30aa6..2a17d185 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
@@ -628,9 +628,9 @@ val insert_on_disk_fwd_def = Define ‘
insert_on_disk_fwd
(key : usize) (value : u64) (st : state) : (state # unit) result =
do
- (st0, hm) <- hashmap_utils_deserialize_fwd st;
+ (st0, hm) <- utils_deserialize_fwd st;
hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
- (st1, _) <- hashmap_utils_serialize_fwd hm0 st0;
+ (st1, _) <- utils_serialize_fwd hm0 st0;
Return (st1, ())
od
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
index d4e43d9a..c19673bb 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
@@ -583,9 +583,9 @@ sig
⊢ ∀key value st.
insert_on_disk_fwd key value st =
do
- (st0,hm) <- hashmap_utils_deserialize_fwd st;
+ (st0,hm) <- utils_deserialize_fwd st;
hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
- (st1,_) <- hashmap_utils_serialize_fwd hm0 st0;
+ (st1,_) <- utils_serialize_fwd hm0 st0;
Return (st1,())
od
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
index f7221d92..9c29c0e0 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
@@ -6,10 +6,10 @@ open hashmapMain_TypesTheory
val _ = new_theory "hashmapMain_Opaque"
-(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd",
+(** [hashmap_main::utils::deserialize]: forward function *)val _ = new_constant ("utils_deserialize_fwd",
“:state -> (state # u64 hashmap_hash_map_t) result”)
-(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd",
+(** [hashmap_main::utils::serialize]: forward function *)val _ = new_constant ("utils_serialize_fwd",
“:u64 hashmap_hash_map_t -> state -> (state # unit) result”)
val _ = export_theory ()
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig b/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig
index f7373609..f7373609 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml b/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml
index 3f8ca9b9..3f8ca9b9 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig b/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig
index a3e770ea..a3e770ea 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig
diff --git a/tests/hol4/misc-loops/Holmakefile b/tests/hol4/loops/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-loops/Holmakefile
+++ b/tests/hol4/loops/Holmakefile
diff --git a/tests/hol4/misc-loops/loops_FunsScript.sml b/tests/hol4/loops/loops_FunsScript.sml
index 65cf77d4..65cf77d4 100644
--- a/tests/hol4/misc-loops/loops_FunsScript.sml
+++ b/tests/hol4/loops/loops_FunsScript.sml
diff --git a/tests/hol4/misc-loops/loops_FunsTheory.sig b/tests/hol4/loops/loops_FunsTheory.sig
index 63fe56c9..63fe56c9 100644
--- a/tests/hol4/misc-loops/loops_FunsTheory.sig
+++ b/tests/hol4/loops/loops_FunsTheory.sig
diff --git a/tests/hol4/misc-loops/loops_TypesScript.sml b/tests/hol4/loops/loops_TypesScript.sml
index e3e5b8d1..e3e5b8d1 100644
--- a/tests/hol4/misc-loops/loops_TypesScript.sml
+++ b/tests/hol4/loops/loops_TypesScript.sml
diff --git a/tests/hol4/misc-loops/loops_TypesTheory.sig b/tests/hol4/loops/loops_TypesTheory.sig
index c3e638d8..c3e638d8 100644
--- a/tests/hol4/misc-loops/loops_TypesTheory.sig
+++ b/tests/hol4/loops/loops_TypesTheory.sig
diff --git a/tests/hol4/misc-no_nested_borrows/Holmakefile b/tests/hol4/no_nested_borrows/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-no_nested_borrows/Holmakefile
+++ b/tests/hol4/no_nested_borrows/Holmakefile
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml b/tests/hol4/no_nested_borrows/noNestedBorrowsScript.sml
index 1b2d6121..1b2d6121 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
+++ b/tests/hol4/no_nested_borrows/noNestedBorrowsScript.sml
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig b/tests/hol4/no_nested_borrows/noNestedBorrowsTheory.sig
index 67368e38..67368e38 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
+++ b/tests/hol4/no_nested_borrows/noNestedBorrowsTheory.sig
diff --git a/tests/hol4/misc-paper/Holmakefile b/tests/hol4/paper/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-paper/Holmakefile
+++ b/tests/hol4/paper/Holmakefile
diff --git a/tests/hol4/misc-paper/paperScript.sml b/tests/hol4/paper/paperScript.sml
index 3ac5b6ca..3ac5b6ca 100644
--- a/tests/hol4/misc-paper/paperScript.sml
+++ b/tests/hol4/paper/paperScript.sml
diff --git a/tests/hol4/misc-paper/paperTheory.sig b/tests/hol4/paper/paperTheory.sig
index 2da80da1..2da80da1 100644
--- a/tests/hol4/misc-paper/paperTheory.sig
+++ b/tests/hol4/paper/paperTheory.sig
diff --git a/tests/hol4/misc-polonius_list/Holmakefile b/tests/hol4/polonius_list/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-polonius_list/Holmakefile
+++ b/tests/hol4/polonius_list/Holmakefile
diff --git a/tests/hol4/misc-polonius_list/poloniusListScript.sml b/tests/hol4/polonius_list/poloniusListScript.sml
index 06876ed4..06876ed4 100644
--- a/tests/hol4/misc-polonius_list/poloniusListScript.sml
+++ b/tests/hol4/polonius_list/poloniusListScript.sml
diff --git a/tests/hol4/misc-polonius_list/poloniusListTheory.sig b/tests/hol4/polonius_list/poloniusListTheory.sig
index 41f21df7..41f21df7 100644
--- a/tests/hol4/misc-polonius_list/poloniusListTheory.sig
+++ b/tests/hol4/polonius_list/poloniusListTheory.sig