author | wenzelm |
Tue, 20 Oct 2009 19:37:09 +0200 | |
changeset 33026 | 8f35633c4922 |
parent 32479 | src/HOL/Isar_examples/ROOT.ML@521cc9bf2958 |
child 37672 | 645eb9fec794 |
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 |
|
32479 | 3 |
no_document use_thys ["../Old_Number_Theory/Primes", "../Old_Number_Theory/Fibonacci"]; |
24228 | 4 |
|
5 |
use_thys [ |
|
31758 | 6 |
"Basic_Logic", |
24228 | 7 |
"Cantor", |
8 |
"Peirce", |
|
9 |
"Drinker", |
|
31758 | 10 |
"Expr_Compiler", |
24228 | 11 |
"Group", |
12 |
"Summation", |
|
31758 | 13 |
"Knaster_Tarski", |
14 |
"Mutilated_Checkerboard", |
|
24228 | 15 |
"Puzzle", |
31758 | 16 |
"Nested_Datatype", |
17 |
"Hoare_Ex" |
|
24228 | 18 |
]; |