diff --git a/.hgignore b/.hgignore
index 5e65870c..4c8efa3f 100644
--- a/.hgignore
+++ b/.hgignore
@@ -10,9 +10,6 @@ parsetab\.py$
 # Generated test files.
 ^tests/\.stable[12]$
 
-# Generated C parser input
-^include/isabelle/.*_pp
-
 # Generate docs
 ^docs/.*\.html$
 ^docs/contents\.js$
diff --git a/include/README b/include/README
index 222ecd0d..359e44ca 100644
--- a/include/README
+++ b/include/README
@@ -14,6 +14,3 @@ environment. For the most part you will need to pay this directory no mind.
 builtin/ - ADL/IDL files that are analogous to the C standard library. You
     should arrange for this to be in the --import-path when runner the tools to
     let users reference files in here with "import <...>" syntax.
-isabelle/ - Theories of various structs and functions in Isabelle. This
-    directory is basically experimentation and most (if not all) of it has been
-    deprecated or migrated to l4.verified.
diff --git a/include/isabelle/GlueMarshal_CAMKES.thy b/include/isabelle/GlueMarshal_CAMKES.thy
deleted file mode 100644
index be1c093e..00000000
--- a/include/isabelle/GlueMarshal_CAMKES.thy
+++ /dev/null
@@ -1,77 +0,0 @@
-(*
- * Copyright 2014, NICTA
- *
- * This software may be distributed and modified according to the terms of
- * the BSD 2-Clause license. Note that NO WARRANTY is provided.
- * See "LICENSE_BSD2.txt" for details.
- *
- * @TAG(NICTA_BSD)
- *)
-
-theory GlueMarshal_CAMKES imports
-    CTranslation
-    Lib_CAMKES
-    "/home/matthew/l4.verified/auto-refine/ValidNoFail"
-    "/home/matthew/l4.verified/auto-refine/AutoRefine" (*FIXME: Remove absolute path *)
-begin
-
-install_C_file "marshal.c_pp"
-(* print_theorems *)
-
-context marshal begin
-local_setup {* AutoRefine.abstract "marshal.c_pp" *}
-(* print_theorems *)
-print_theorems
-
-(* Dereference a pointer *)
-abbreviation "deref s x \<equiv> h_val (hrs_mem (t_hrs_' s)) x"
-abbreviation "byte_cast x \<equiv> ((ptr_coerce x)::8 word ptr)"
-
-lemma memcpy_char:
-  "\<lbrace> \<lambda>s. c_guard (x::8 word ptr) \<and>
-         c_guard (y::8 word ptr) \<and>
-         unat sz = size_of TYPE(8 word) \<and>
-         P (deref s x) \<and>
-         x \<noteq> y\<rbrace>
-      memcpy' (ptr_coerce y) (ptr_coerce x) sz
-   \<lbrace>\<lambda> _ s. P (deref s y) \<rbrace>!"
-  (* Evaluate sz *)
-  apply (clarsimp simp:unat_eq_1(2))
-
-  unfolding memcpy'_def apply clarsimp
-  apply wp
-
-  (* Unroll the loop twice *)
-  apply (subst whileLoop_unfold', wp)
-     apply (subst whileLoop_unfold', wp)
-
-  (* The remaining loop is never encountered *)
-       apply (rule validNF_false_pre)
-      apply wp
-
-  (* Finally we're left with the single assignment *)
-  apply (clarsimp simp:ptr_add_0_id hrs_mem_update h_val_heap_update)
- done
-    
-lemma marshal_unmarshal_char:
-  "\<lbrace> \<lambda>s. c_guard (x::8 word ptr) \<and>
-         c_guard (y::8 word ptr) \<and>
-         c_guard (buffer::8 word ptr) \<and>
-         unat sz = size_of TYPE(8 word) \<and>
-         P (deref s x) \<and>
-         x \<noteq> y  \<and>
-         x \<noteq> buffer \<and>
-         y \<noteq> buffer \<rbrace>
-      do
-        camkes_marshal' (ptr_coerce buffer) (ptr_coerce x) sz;
-        camkes_unmarshal' (ptr_coerce buffer) (ptr_coerce y) sz
-      od
-   \<lbrace> \<lambda>_ s. P (deref s y) \<rbrace>!"
-  unfolding camkes_marshal'_def camkes_unmarshal'_def
-  apply (wp add:memcpy_char del:validNF_prop)
-  apply clarsimp
- done
-
-end
-
-end
diff --git a/include/isabelle/Lib_CAMKES.thy b/include/isabelle/Lib_CAMKES.thy
deleted file mode 100644
index 7df45335..00000000
--- a/include/isabelle/Lib_CAMKES.thy
+++ /dev/null
@@ -1,38 +0,0 @@
-(*
- * Copyright 2014, NICTA
- *
- * This software may be distributed and modified according to the terms of
- * the BSD 2-Clause license. Note that NO WARRANTY is provided.
- * See "LICENSE_BSD2.txt" for details.
- *
- * @TAG(NICTA_BSD)
- *)
-
-theory Lib_CAMKES imports
-    "/home/matthew/l4.verified/auto-refine/ValidNoFail"
-    CTranslation
-begin
-
-(* Lemmas that belong somewhere else. If you are browsing this file and know
- * where a lemma should go, feel free to move it if you can do so without
- * breaking my proofs.
- *)
-
-(* Adding 0 to a pointer leaves it unchanged *)
-lemma ptr_add_0_id:"x +\<^isub>p 0 = x"
-  by (case_tac x, simp)
-
-(* All non-null byte pointers are well-formed *)
-lemma byte_ptr_ok:"ptr_val (x::8 word ptr) \<noteq> 0 \<Longrightarrow> c_guard x"
-  unfolding c_guard_def c_null_guard_def ptr_aligned_def
-  by (clarsimp simp: intvl_Suc simp del:word_neq_0_conv)
-
-lemma no_fail_false[wp]:"no_fail (\<lambda>s. False) f"
- by (clarsimp simp:no_fail_def)
-
-lemma validNF_false_pre:"\<lbrace>\<lambda>_. False\<rbrace> a \<lbrace>P\<rbrace>!"
-  apply rule
-  apply (wp|simp)+
- done
-
-end
diff --git a/include/isabelle/Makefile b/include/isabelle/Makefile
deleted file mode 100644
index 1538ae53..00000000
--- a/include/isabelle/Makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-#
-# Copyright 2014, NICTA
-#
-# This software may be distributed and modified according to the terms of
-# the BSD 2-Clause license. Note that NO WARRANTY is provided.
-# See "LICENSE_BSD2.txt" for details.
-#
-# @TAG(NICTA_BSD)
-#
-
-default: marshal.c_pp
-
-%.h_pp: ../camkes/%.h
-	cpp $^ >$@
-
-%.c_pp: ../src/%.c
-	cpp -I../ $^ >$@
-
-clean:
-	rm -f marshal.c_pp