equal
deleted
inserted
replaced
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Miscellaneous Isabelle/Isar examples for Higher-Order Logic. |
5 Miscellaneous Isabelle/Isar examples for Higher-Order Logic. |
6 *) |
6 *) |
7 |
7 |
8 time_use_thy "BasicLogic"; |
8 no_document use_thys ["../NumberTheory/Primes", "../NumberTheory/Fibonacci"]; |
9 time_use_thy "Cantor"; |
9 |
10 time_use_thy "Peirce"; |
10 use_thys [ |
11 time_use_thy "Drinker"; |
11 "BasicLogic", |
12 time_use_thy "ExprCompiler"; |
12 "Cantor", |
13 time_use_thy "Group"; |
13 "Peirce", |
14 time_use_thy "Summation"; |
14 "Drinker", |
15 time_use_thy "KnasterTarski"; |
15 "ExprCompiler", |
16 time_use_thy "MutilatedCheckerboard"; |
16 "Group", |
17 with_path "../NumberTheory" (no_document time_use_thy) "Primes"; |
17 "Summation", |
18 with_path "../NumberTheory" time_use_thy "Fibonacci"; |
18 "KnasterTarski", |
19 time_use_thy "Puzzle"; |
19 "MutilatedCheckerboard", |
20 time_use_thy "NestedDatatype"; |
20 "Puzzle", |
21 time_use_thy "HoareEx"; |
21 "NestedDatatype", |
|
22 "HoareEx" |
|
23 ]; |