author | nipkow |
Tue, 02 Sep 2008 21:31:28 +0200 | |
changeset 28091 | 50f2d6ba024c |
parent 27367 | a75d71c73362 |
child 28228 | 7ebe8dc06cbb |
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 |
28091
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27367
diff
changeset
|
8 |
imports Plain Map Nat_Int_Bij Recdef |
15131 | 9 |
begin |
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
10 |
|
25223 | 11 |
ML {* val HOL_proofs = ! Proofterm.proofs *} |
23165 | 12 |
|
27367 | 13 |
text {* See further \cite{Nipkow-et-al:2002:tutorial} *} |
25964 | 14 |
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
15 |
end |