| author | wenzelm | 
| Fri, 30 Dec 2022 16:23:32 +0100 | |
| changeset 76827 | a150dd0ebdd3 | 
| parent 69319 | baccaf89ca0d | 
| permissions | -rw-r--r-- | 
| 
62286
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
1  | 
chapter HOL  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
2  | 
|
| 
65573
 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
 
wenzelm 
parents: 
62286 
diff
changeset
 | 
3  | 
session "HOL-Datatype_Benchmark" in Datatype_Benchmark = "HOL-Library" +  | 
| 69319 | 4  | 
description "  | 
| 
62286
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
5  | 
Big (co)datatypes.  | 
| 69319 | 6  | 
"  | 
| 
62286
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
7  | 
theories  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
8  | 
Brackin  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
9  | 
IsaFoR  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
10  | 
Misc_N2M  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
11  | 
|
| 
65573
 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
 
wenzelm 
parents: 
62286 
diff
changeset
 | 
12  | 
session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = "HOL-Library" +  | 
| 
62286
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
13  | 
theories [quick_and_dirty]  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
14  | 
Find_Unused_Assms_Examples  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
15  | 
Needham_Schroeder_No_Attacker_Example  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
16  | 
Needham_Schroeder_Guided_Attacker_Example  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
17  | 
Needham_Schroeder_Unguided_Attacker_Example  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
18  | 
|
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
19  | 
session "HOL-Record_Benchmark" in Record_Benchmark = HOL +  | 
| 69319 | 20  | 
description "  | 
| 
62286
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
21  | 
Big records.  | 
| 69319 | 22  | 
"  | 
| 
62286
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
theories  | 
| 
 
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
 
wenzelm 
parents:  
diff
changeset
 | 
24  | 
Record_Benchmark  |