src/HOL/ROOT

--- a/src/HOL/ROOT	Thu May 01 22:41:03 2014 +0200
+++ b/src/HOL/ROOT	Thu May 01 22:56:59 2014 +0200
@@ -578,6 +578,7 @@
     SVC_Oracle
     Simps_Case_Conv_Examples
     ML
+    SAT_Examples
   theories [skip_proofs = false]
     Meson_Test
   theories [condition = SVC_HOME]
@@ -585,10 +586,6 @@
   theories [condition = ZCHAFF_HOME]
     (*requires zChaff (or some other reasonably fast SAT solver)*)
     Sudoku
-(* FIXME
-(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
-    SAT_Examples
-*)
   document_files "root.bib" "root.tex"
 
 session "HOL-Isar_Examples" in Isar_Examples = HOL +