1 files changed, 0 insertions, 14 deletions
diff --git a/cheri/sail_latex/sailfnexecuteTLBP.tex b/cheri/sail_latex/sailfnexecuteTLBP.tex
deleted file mode 100644
index 1c781dda..00000000
--- a/cheri/sail_latex/sailfnexecuteTLBP.tex
+++ /dev/null
@@ -1,14 +0,0 @@
-function clause #\hyperref[zexecute]{execute}# (#\hyperref[zTLBP]{TLBP}#()) = {
-  #\hyperref[zcheckCPzeroAccess]{checkCP0Access}#();
-  let result = #\hyperref[ztlbSearch]{tlbSearch}#(TLBEntryHi.#\hyperref[zbits]{bits}#()) in
-  match result {
-    (#\hyperref[zSome]{Some}#(idx))  => {
-      TLBProbe = [bitzero];
-      TLBIndex = idx;
-    },
-    #\hyperref[zNone]{None}#()  => {
-      TLBProbe = [bitone];
-      TLBIndex = 0b000000;
-    }
-  }
-}