diff --git a/examples/HOL_Enum_wp/ROOT b/examples/HOL_Enum_wp/ROOT
new file mode 100644
index 0000000..a6adf69
--- /dev/null
+++ b/examples/HOL_Enum_wp/ROOT
@@ -0,0 +1,5 @@
+session HOL_Enum_wp = HOL_Pre_Enum +
+  options [strict_facts,export_theory,export_proofs,record_proofs=2]
+  sessions HOL
+  theories
+    HOL.Enum
diff --git a/examples/ROOTS b/examples/ROOTS
index 2d25b5b..2747393 100644
--- a/examples/ROOTS
+++ b/examples/ROOTS
@@ -2,3 +2,4 @@ HOL_wp
 HOL_Groups_wp
 HOL-Library_wp
 HOL_Pre_Enum
+HOL_Enum_wp