summaryrefslogtreecommitdiff
path: root/tests/hol4
diff options
context:
space:
mode:
authorSon HO2024-05-27 09:39:39 +0200
committerGitHub2024-05-27 09:39:39 +0200
commitaeff52b13b9b3068efcc4a805a9786bf2053d141 (patch)
tree229e6fc225bf8456a01985cd3b583e510acc3886 /tests/hol4
parent3ff6d93822fe5b2e233d4b12b88b38839c8533c5 (diff)
parent4971b7edf4538144df735f9fa5327fe4d0e2e003 (diff)
Merge branch 'main' into unsigned-max
Diffstat (limited to 'tests/hol4')
-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)0
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig (renamed from tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig)0
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml (renamed from tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml)0
-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
31 files changed, 0 insertions, 0 deletions
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..c1e30aa6 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
index d4e43d9a..d4e43d9a 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
index f7221d92..f7221d92 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
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