added HOL_Enum_wp

Deducteam · Nov 13, 2023 · e9ad61f · e9ad61f
1 parent fd173fe
commit e9ad61f
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/examples/HOL_Enum_wp/ROOT 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
@@ -2,3 +2,4 @@ HOL_wp
 HOL_Groups_wp
 HOL-Library_wp
 HOL_Pre_Enum
+HOL_Enum_wp