src/HOL/ROOT
changeset 56815 848d507584db
parent 56801 8dd9df88f647
child 56818 689a3eeb6f9e
     1.1 --- a/src/HOL/ROOT	Thu May 01 22:41:03 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Thu May 01 22:56:59 2014 +0200
     1.3 @@ -578,6 +578,7 @@
     1.4      SVC_Oracle
     1.5      Simps_Case_Conv_Examples
     1.6      ML
     1.7 +    SAT_Examples
     1.8    theories [skip_proofs = false]
     1.9      Meson_Test
    1.10    theories [condition = SVC_HOME]
    1.11 @@ -585,10 +586,6 @@
    1.12    theories [condition = ZCHAFF_HOME]
    1.13      (*requires zChaff (or some other reasonably fast SAT solver)*)
    1.14      Sudoku
    1.15 -(* FIXME
    1.16 -(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
    1.17 -    SAT_Examples
    1.18 -*)
    1.19    document_files "root.bib" "root.tex"
    1.20  
    1.21  session "HOL-Isar_Examples" in Isar_Examples = HOL +