diff --git a/spec/abstract/X64/ArchInvocation_A.thy b/spec/abstract/X64/ArchInvocation_A.thy
index ef5584b45..6ecbe434f 100644
--- a/spec/abstract/X64/ArchInvocation_A.thy
+++ b/spec/abstract/X64/ArchInvocation_A.thy
@@ -73,11 +73,11 @@ datatype page_invocation
      | PageUnmap 
          (page_unmap_cap: arch_cap)
          (page_unmap_cap_slot: cslot_ptr)
-     | PageIOMap 
+(*     | PageIOMap 
          (page_iomap_cap: cap)
          (page_iomap_ct_clot: cslot_ptr)
          (page_iomap_asid: iopte)
-         (page_iomap_entries: "obj_ref") (*FIXME: double check plz*)
+         (page_iomap_entries: "obj_ref") (*FIXME: double check plz*)*)
      | PageGetAddr
          (page_get_paddr: obj_ref)
 
diff --git a/spec/abstract/X64/Arch_A.thy b/spec/abstract/X64/Arch_A.thy
index 8d44c3637..fe5db5195 100644
--- a/spec/abstract/X64/Arch_A.thy
+++ b/spec/abstract/X64/Arch_A.thy
@@ -164,7 +164,7 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
             (case mapped of Some (asid, vaddr) \<Rightarrow> unmap_page sz asid vaddr base
                           | None \<Rightarrow> return ())
           | _ \<Rightarrow> fail)
-  | PageIOMap asid cap ct_slot entries \<Rightarrow> undefined (* FIXME unimplemented *)
+(*  | PageIOMap asid cap ct_slot entries \<Rightarrow> undefined (* FIXME unimplemented *)*)
   | PageGetAddr ptr \<Rightarrow> do
       paddr \<leftarrow> return $ fromPAddr $ addrFromPPtr ptr;
       ct \<leftarrow> gets cur_thread;
diff --git a/spec/machine/X64/MachineOps.thy b/spec/machine/X64/MachineOps.thy
index dfece5f6d..28f68cec1 100644
--- a/spec/machine/X64/MachineOps.thy
+++ b/spec/machine/X64/MachineOps.thy
@@ -255,10 +255,13 @@ mfence :: "unit machine_monad"
 where
 "mfence \<equiv> undefined"
 
+consts'
+  invalidateTLBEntry_impl :: "word64 \<Rightarrow> unit machine_rest_monad"
+
 definition
 invalidateTLBEntry :: "word64 \<Rightarrow> unit machine_monad"
 where
-"invalidateTLBEntry vptr \<equiv> undefined vptr"
+"invalidateTLBEntry vptr \<equiv> machine_op_lift (invalidateTLBEntry_impl vptr)"
 
 definition
 firstValidIODomain :: "word16"