summaryrefslogtreecommitdiff
path: root/tests/hol4/misc-external
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hol4/misc-external/external_FunsScript.sml1
-rw-r--r--tests/hol4/misc-external/external_OpaqueScript.sml1
-rw-r--r--tests/hol4/misc-external/external_TypesScript.sml1
3 files changed, 0 insertions, 3 deletions
diff --git a/tests/hol4/misc-external/external_FunsScript.sml b/tests/hol4/misc-external/external_FunsScript.sml
index f3692ee2..65433aff 100644
--- a/tests/hol4/misc-external/external_FunsScript.sml
+++ b/tests/hol4/misc-external/external_FunsScript.sml
@@ -1,4 +1,3 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [external]: function definitions *)
open primitivesLib divDefLib
open external_TypesTheory external_OpaqueTheory
diff --git a/tests/hol4/misc-external/external_OpaqueScript.sml b/tests/hol4/misc-external/external_OpaqueScript.sml
index b5a6d91d..e5faf97c 100644
--- a/tests/hol4/misc-external/external_OpaqueScript.sml
+++ b/tests/hol4/misc-external/external_OpaqueScript.sml
@@ -1,4 +1,3 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [external]: external function declarations *)
open primitivesLib divDefLib
open external_TypesTheory
diff --git a/tests/hol4/misc-external/external_TypesScript.sml b/tests/hol4/misc-external/external_TypesScript.sml
index d290c3f6..207eea8d 100644
--- a/tests/hol4/misc-external/external_TypesScript.sml
+++ b/tests/hol4/misc-external/external_TypesScript.sml
@@ -1,4 +1,3 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [external]: type definitions *)
open primitivesLib divDefLib