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