Rename some subdirectories for consistency

3 files changed, 0 insertions, 162 deletions

diff --git a/tests/hol4/misc-polonius_list/Holmakefile b/tests/hol4/misc-polonius_list/Holmakefile
deleted file mode 100644
index 3c4b8973..00000000
--- a/tests/hol4/misc-polonius_list/Holmakefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# This file was automatically generated - modify ../Holmakefile.template instead
-INCLUDES =  ../../../backends/hol4
-
-all: $(DEFAULT_TARGETS)
-.PHONY: all
diff --git a/tests/hol4/misc-polonius_list/poloniusListScript.sml b/tests/hol4/misc-polonius_list/poloniusListScript.sml
deleted file mode 100644
index 06876ed4..00000000
--- a/tests/hol4/misc-polonius_list/poloniusListScript.sml
+++ /dev/null
@@ -1,37 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [polonius_list] *)
-open primitivesLib divDefLib
-
-val _ = new_theory "poloniusList"
-
-
-Datatype:
-  (** [polonius_list::List] *)
-  list_t = | ListCons 't list_t | ListNil
-End
-
-val [get_list_at_x_fwd_def] = DefineDiv ‘
-  (** [polonius_list::get_list_at_x]: forward function *)
-  get_list_at_x_fwd (ls : u32 list_t) (x : u32) : u32 list_t result =
-    (case ls of
-    | ListCons hd tl =>
-      if hd = x then Return (ListCons hd tl) else get_list_at_x_fwd tl x
-    | ListNil => Return ListNil)
-’
-
-val [get_list_at_x_back_def] = DefineDiv ‘
-  (** [polonius_list::get_list_at_x]: backward function 0 *)
-  get_list_at_x_back
-    (ls : u32 list_t) (x : u32) (ret : u32 list_t) : u32 list_t result =
-    (case ls of
-    | ListCons hd tl =>
-      if hd = x
-      then Return ret
-      else (do
-            tl0 <- get_list_at_x_back tl x ret;
-            Return (ListCons hd tl0)
-            od)
-    | ListNil => Return ret)
-’
-
-val _ = export_theory ()
diff --git a/tests/hol4/misc-polonius_list/poloniusListTheory.sig b/tests/hol4/misc-polonius_list/poloniusListTheory.sig
deleted file mode 100644
index 41f21df7..00000000
--- a/tests/hol4/misc-polonius_list/poloniusListTheory.sig
+++ /dev/null
@@ -1,120 +0,0 @@
-signature poloniusListTheory =
-sig
-  type thm = Thm.thm
-  
-  (*  Definitions  *)
-    val get_list_at_x_back_def : thm
-    val get_list_at_x_fwd_def : thm
-    val list_t_TY_DEF : thm
-    val list_t_case_def : thm
-    val list_t_size_def : thm
-  
-  (*  Theorems  *)
-    val datatype_list_t : thm
-    val list_t_11 : thm
-    val list_t_Axiom : thm
-    val list_t_case_cong : thm
-    val list_t_case_eq : thm
-    val list_t_distinct : thm
-    val list_t_induction : thm
-    val list_t_nchotomy : thm
-  
-  val poloniusList_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [divDef] Parent theory of "poloniusList"
-   
-   [get_list_at_x_back_def]  Definition
-      
-      ⊢ ∀ls x ret.
-          get_list_at_x_back ls x ret =
-          case ls of
-            ListCons hd tl =>
-              if hd = x then Return ret
-              else
-                do
-                  tl0 <- get_list_at_x_back tl x ret;
-                  Return (ListCons hd tl0)
-                od
-          | ListNil => Return ret
-   
-   [get_list_at_x_fwd_def]  Definition
-      
-      ⊢ ∀ls x.
-          get_list_at_x_fwd ls x =
-          case ls of
-            ListCons hd tl =>
-              if hd = x then Return (ListCons hd tl)
-              else get_list_at_x_fwd tl x
-          | ListNil => Return ListNil
-   
-   [list_t_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0'.
-                 ∀ $var$('list_t').
-                   (∀a0'.
-                      (∃a0 a1.
-                         a0' =
-                         (λa0 a1.
-                              ind_type$CONSTR 0 a0
-                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
-                           a0 a1 ∧ $var$('list_t') a1) ∨
-                      a0' =
-                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
-                      $var$('list_t') a0') ⇒
-                   $var$('list_t') a0') rep
-   
-   [list_t_case_def]  Definition
-      
-      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
-        ∀f v. list_t_CASE ListNil f v = v
-   
-   [list_t_size_def]  Definition
-      
-      ⊢ (∀f a0 a1.
-           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
-        ∀f. list_t_size f ListNil = 0
-   
-   [datatype_list_t]  Theorem
-      
-      ⊢ DATATYPE (list_t ListCons ListNil)
-   
-   [list_t_11]  Theorem
-      
-      ⊢ ∀a0 a1 a0' a1'.
-          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
-   
-   [list_t_Axiom]  Theorem
-      
-      ⊢ ∀f0 f1. ∃fn.
-          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
-          fn ListNil = f1
-   
-   [list_t_case_cong]  Theorem
-      
-      ⊢ ∀M M' f v.
-          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
-          (M' = ListNil ⇒ v = v') ⇒
-          list_t_CASE M f v = list_t_CASE M' f' v'
-   
-   [list_t_case_eq]  Theorem
-      
-      ⊢ list_t_CASE x f v = v' ⇔
-        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
-   
-   [list_t_distinct]  Theorem
-      
-      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
-   
-   [list_t_induction]  Theorem
-      
-      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
-   
-   [list_t_nchotomy]  Theorem
-      
-      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
-   
-   
-*)
-end