author | chaieb |
Wed, 31 Oct 2007 12:19:41 +0100 | |
changeset 25252 | 833abbc3e733 |
parent 25223 | 7463251e7273 |
child 25964 | 080f89d89990 |
permissions | -rw-r--r-- |
17602 | 1 |
(* Title: HOL/Main.thy |
2 |
ID: $Id$ |
|
3 |
*) |
|
9619 | 4 |
|
12024 | 5 |
header {* Main HOL *} |
6 |
||
15131 | 7 |
theory Main |
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24644
diff
changeset
|
8 |
imports Map |
15131 | 9 |
begin |
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
10 |
|
12024 | 11 |
text {* |
12 |
Theory @{text Main} includes everything. Note that theory @{text |
|
13 |
PreList} already includes most HOL theories. |
|
19608 | 14 |
*} |
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
15 |
|
25223 | 16 |
ML {* val HOL_proofs = ! Proofterm.proofs *} |
23165 | 17 |
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
18 |
end |