author | wenzelm |
Tue, 07 Dec 1999 12:13:09 +0100 | |
changeset 8051 | 5724bea1da53 |
parent 8037 | 18f10850aca5 |
child 8137 | fb6fe34060ca |
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"; |
15 |
time_use_thy "MutilatedCheckerboard"; |
|
7443 | 16 |
with_path "../Induct" time_use_thy "MultisetOrder"; |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
7443
diff
changeset
|
17 |
with_path "../W0" time_use_thy "W_correct"; |
8051 | 18 |
with_path "../ex" time_use_thy "Fibonacci"; |
8020 | 19 |
time_use_thy "Puzzle"; |
8037 | 20 |
time_use_thy "Minimal"; |