some isabelle/hol verificationHEADmain

doesn't do much, just proves that the find function won't cause an
error.

also removes all uses of rust traits, since these are currently broken
on the aeneas side.

1 files changed, 7 insertions, 0 deletions

diff --git a/ROOT b/ROOT
new file mode 100644
index 0000000..18d302f
--- /dev/null
+++ b/ROOT
@@ -0,0 +1,7 @@
+session "avl-verification" = "Aeneas" +
+  options [document = pdf, document_output = "output"]
+  theories
+    Notraits
+    Verification
+  document_files
+    "root.tex"