author | bulwahn |
Wed, 20 Jan 2010 11:56:45 +0100 | |
changeset 34948 | 2d5f2a9f7601 |
parent 34897 | cf9e3426c7b1 |
child 35222 | 4f1fba00f66d |
permissions | -rw-r--r-- |
12024 | 1 |
header {* Main HOL *} |
2 |
||
15131 | 3 |
theory Main |
34897
cf9e3426c7b1
reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
blanchet
parents:
33567
diff
changeset
|
4 |
imports Plain Predicate_Compile Nitpick |
15131 | 5 |
begin |
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
6 |
|
29304 | 7 |
text {* |
8 |
Classical Higher-order Logic -- only ``Main'', excluding real and |
|
9 |
complex numbers etc. |
|
10 |
*} |
|
11 |
||
27367 | 12 |
text {* See further \cite{Nipkow-et-al:2002:tutorial} *} |
25964 | 13 |
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
14 |
end |