1chapter HOL 2 3session "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 12session "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 19session "HOL-Record_Benchmark" in Record_Benchmark = HOL + 20 description " 21 Big records. 22 " 23 theories 24 Record_Benchmark 25