src/HOL/ROOT
changeset 48901 5e0455e29339
parent 48765 fb1ed5230abc
child 48932 c6e679443adc
     1.1 --- a/src/HOL/ROOT	Thu Aug 23 12:44:52 2012 +0200
     1.2 +++ b/src/HOL/ROOT	Thu Aug 23 12:55:23 2012 +0200
     1.3 @@ -2,7 +2,11 @@
     1.4    description {* Classical Higher-order Logic *}
     1.5    options [document_graph]
     1.6    theories Complex_Main
     1.7 -  files "document/root.bib" "document/root.tex"
     1.8 +  files
     1.9 +    "Tools/Quickcheck/Narrowing_Engine.hs"
    1.10 +    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    1.11 +    "document/root.bib"
    1.12 +    "document/root.tex"
    1.13  
    1.14  session "HOL-Base" = Pure +
    1.15    description {* Raw HOL base, with minimal tools *}
    1.16 @@ -18,11 +22,17 @@
    1.17    description {* HOL side-entry for Main only, without Complex_Main *}
    1.18    options [document = false]
    1.19    theories Main
    1.20 +  files
    1.21 +    "Tools/Quickcheck/Narrowing_Engine.hs"
    1.22 +    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    1.23  
    1.24  session "HOL-Proofs" = Pure +
    1.25    description {* HOL-Main with explicit proof terms *}
    1.26    options [document = false, proofs = 2, parallel_proofs = 0]
    1.27    theories Main
    1.28 +  files
    1.29 +    "Tools/Quickcheck/Narrowing_Engine.hs"
    1.30 +    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    1.31  
    1.32  session "HOL-Library" in Library = HOL +
    1.33    description {* Classical Higher-order Logic -- batteries included *}