src/HOL/ROOT
changeset 65509 ffedb16f382f
parent 65485 8c7bc3a13513
child 65515 f595b7532dc9
child 65530 09c00a304c00
equal deleted inserted replaced
65508:a72ab197e681 65509:ffedb16f382f
    18   description {*
    18   description {*
    19     HOL-Main with explicit proof terms.
    19     HOL-Main with explicit proof terms.
    20   *}
    20   *}
    21   options [document = false, theory_qualifier = "HOL",
    21   options [document = false, theory_qualifier = "HOL",
    22     quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
    22     quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
    23   theories "~~/src/HOL/Library/Old_Datatype"
    23   sessions "HOL-Library"
       
    24   theories "HOL-Library.Old_Datatype"
    24   files
    25   files
    25     "Tools/Quickcheck/Narrowing_Engine.hs"
    26     "Tools/Quickcheck/Narrowing_Engine.hs"
    26     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    27     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    27 
    28 
    28 session "HOL-Library" (main timing) in Library = HOL +
    29 session "HOL-Library" (main timing) in Library = HOL +