src/Benchmarks/ROOT
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 66946 3d8fd98c7c86
child 69272 15e9ed5b28fb
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 chapter HOL
     2 
     3 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = "HOL-Library" +
     4   description {*
     5     Big (co)datatypes.
     6   *}
     7   theories
     8     Brackin
     9     IsaFoR
    10     Misc_N2M
    11 
    12 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = "HOL-Library" +
    13   theories [quick_and_dirty]
    14     Find_Unused_Assms_Examples
    15     Needham_Schroeder_No_Attacker_Example
    16     Needham_Schroeder_Guided_Attacker_Example
    17     Needham_Schroeder_Unguided_Attacker_Example
    18 
    19 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
    20   description {*
    21     Big records.
    22   *}
    23   theories
    24     Record_Benchmark