author | wenzelm |
Wed, 05 Apr 2000 21:06:52 +0200 | |
changeset 8675 | a2ff2301d65e |
parent 8137 | fb6fe34060ca |
child 8782 | 86b6b6e712ee |
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"; |
8675 | 20 |
time_use_thy "NestedDatatype"; |