summaryrefslogtreecommitdiff
path: root/tests/hol4/betree
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hol4/betree/betreeMain_FunsScript.sml1
-rw-r--r--tests/hol4/betree/betreeMain_OpaqueScript.sml1
-rw-r--r--tests/hol4/betree/betreeMain_TypesScript.sml1
3 files changed, 0 insertions, 3 deletions
diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml
index bd16c16c..ae3c4de2 100644
--- a/tests/hol4/betree/betreeMain_FunsScript.sml
+++ b/tests/hol4/betree/betreeMain_FunsScript.sml
@@ -1,4 +1,3 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [betree_main]: function definitions *)
open primitivesLib divDefLib
open betreeMain_TypesTheory betreeMain_OpaqueTheory
diff --git a/tests/hol4/betree/betreeMain_OpaqueScript.sml b/tests/hol4/betree/betreeMain_OpaqueScript.sml
index 1d16db4c..04a547e1 100644
--- a/tests/hol4/betree/betreeMain_OpaqueScript.sml
+++ b/tests/hol4/betree/betreeMain_OpaqueScript.sml
@@ -1,4 +1,3 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [betree_main]: external function declarations *)
open primitivesLib divDefLib
open betreeMain_TypesTheory
diff --git a/tests/hol4/betree/betreeMain_TypesScript.sml b/tests/hol4/betree/betreeMain_TypesScript.sml
index 779f6abb..685df462 100644
--- a/tests/hol4/betree/betreeMain_TypesScript.sml
+++ b/tests/hol4/betree/betreeMain_TypesScript.sml
@@ -1,4 +1,3 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [betree_main]: type definitions *)
open primitivesLib divDefLib