src/HOL/ROOT

     Parallel_Example
     IArray_Examples
     SVC_Oracle
     Simps_Case_Conv_Examples
     ML
+    SAT_Examples
   theories [skip_proofs = false]
     Meson_Test
   theories [condition = SVC_HOME]
     svc_test
   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 +
   description {*
     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.