author | paulson |
Wed, 13 Sep 2000 18:45:10 +0200 | |
changeset 9942 | 87f0809a06a9 |
parent 8814 | 0a5edcbe0695 |
child 10145 | e44b8b7cb01b |
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 |
ID: $Id$ |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
5 |
Miscellaneous Isabelle/Isar examples for Higher-Order Logic. |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
6 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
7 |
|
7384 | 8 |
time_use_thy "BasicLogic"; |
7800 | 9 |
time_use_thy "Cantor"; |
7384 | 10 |
time_use_thy "Peirce"; |
11 |
time_use_thy "ExprCompiler"; |
|
12 |
time_use_thy "Group"; |
|
7443 | 13 |
time_use_thy "Summation"; |
7384 | 14 |
time_use_thy "KnasterTarski"; |
8814 | 15 |
time_use_thy "MutilatedCheckerboard"; |
9942
87f0809a06a9
moved Primes, Fib, Factorization to HOL/NumberTheory
paulson
parents:
8814
diff
changeset
|
16 |
with_path "../Induct" time_use_thy "MultisetOrder"; |
87f0809a06a9
moved Primes, Fib, Factorization to HOL/NumberTheory
paulson
parents:
8814
diff
changeset
|
17 |
with_path "../W0" time_use_thy "W_correct"; |
87f0809a06a9
moved Primes, Fib, Factorization to HOL/NumberTheory
paulson
parents:
8814
diff
changeset
|
18 |
with_path "../NumberTheory" time_use_thy "Fibonacci"; |
8020 | 19 |
time_use_thy "Puzzle"; |
8675 | 20 |
time_use_thy "NestedDatatype"; |