diff options
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 |