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, 17 insertions, 0 deletions

diff --git a/notes.md b/notes.md
index 942e1ca..977cbd0 100644
--- a/notes.md
+++ b/notes.md
@@ -1,3 +1,20 @@
+# Isabelle
+
+build with
+
+```
+❯ isabelle build -d path/to/aeneas/backends/IsabelleHOL/ -D .
+```
+
+or open in jedit via
+
+```
+❯ isabelle jedit -d path/to/aeneas/backends/IsabelleHOL/ Verification.thy
+```
+
+(there is no nix flake output for Isabelle. Isabelle is unpackagable and the
+one that exists in nixpkgs is but a mirage)
+
 # Formalization notes
 
 - Inhabited is not synthesized systematically for any type.