From 60ec110ebfe85ecbadf2641bdc5315c619766f0e Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Sat, 29 Jun 2024 22:05:40 +0200
Subject: some isabelle/hol verification

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.
---
 ROOT | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 ROOT

(limited to 'ROOT')

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"
-- 
cgit v1.2.3