author | wenzelm |
Sun, 06 May 2012 13:22:37 +0200 | |
changeset 47871 | 861dc9184920 |
parent 46582 | dcc312f22ee8 |
permissions | -rw-r--r-- |
33026 | 1 |
(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *) |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
|
46582 | 3 |
no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"]; |
24228 | 4 |
|
5 |
use_thys [ |
|
31758 | 6 |
"Basic_Logic", |
24228 | 7 |
"Cantor", |
8 |
"Drinker", |
|
31758 | 9 |
"Expr_Compiler", |
47871 | 10 |
"Fibonacci", |
24228 | 11 |
"Group", |
47871 | 12 |
"Group_Context", |
13 |
"Group_Notepad", |
|
14 |
"Hoare_Ex", |
|
31758 | 15 |
"Knaster_Tarski", |
16 |
"Mutilated_Checkerboard", |
|
47871 | 17 |
"Nested_Datatype", |
18 |
"Peirce", |
|
24228 | 19 |
"Puzzle", |
47871 | 20 |
"Summation" |
24228 | 21 |
]; |