author | wenzelm |
Tue, 28 Sep 1999 14:24:22 +0200 | |
changeset 7621 | 4074bc1e380d |
parent 7443 | e5356e73f57a |
child 7800 | 8ee919e42174 |
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"; |
9 |
time_use_thy "Peirce"; |
|
10 |
time_use_thy "Cantor"; |
|
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"; |