author | haftmann |
Tue, 01 Sep 2009 15:39:33 +0200 | |
changeset 32479 | 521cc9bf2958 |
parent 31758 | 3edd5f813f01 |
permissions | -rw-r--r-- |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Isar_examples/ROOT.ML |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
Miscellaneous Isabelle/Isar examples for Higher-Order Logic. |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
5 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
6 |
|
32479 | 7 |
no_document use_thys ["../Old_Number_Theory/Primes", "../Old_Number_Theory/Fibonacci"]; |
24228 | 8 |
|
9 |
use_thys [ |
|
31758 | 10 |
"Basic_Logic", |
24228 | 11 |
"Cantor", |
12 |
"Peirce", |
|
13 |
"Drinker", |
|
31758 | 14 |
"Expr_Compiler", |
24228 | 15 |
"Group", |
16 |
"Summation", |
|
31758 | 17 |
"Knaster_Tarski", |
18 |
"Mutilated_Checkerboard", |
|
24228 | 19 |
"Puzzle", |
31758 | 20 |
"Nested_Datatype", |
21 |
"Hoare_Ex" |
|
24228 | 22 |
]; |