changeset 46582 | dcc312f22ee8 |
parent 37672 | 645eb9fec794 |
child 47871 | 861dc9184920 |
46581:1544a8703787 | 46582:dcc312f22ee8 |
---|---|
1 (* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *) |
1 (* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *) |
2 |
2 |
3 no_document use_thys ["../Number_Theory/Primes"]; |
3 no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"]; |
4 |
4 |
5 use_thys [ |
5 use_thys [ |
6 "Basic_Logic", |
6 "Basic_Logic", |
7 "Cantor", |
7 "Cantor", |
8 "Peirce", |
8 "Peirce", |