src/Benchmarks/ROOT
author wenzelm
Thu Feb 28 21:59:58 2019 +0100 (6 months ago ago)
changeset 70031 5f993636ac07
parent 69329 baccaf89ca0d
permissions -rw-r--r--
tuned proofs -- eliminated odd case_tac;
     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