| author | krauss |
| Sat, 27 Dec 2008 17:49:15 +0100 | |
| changeset 29183 | f1648e009dc1 |
| parent 28263 | 69eaa97e7e96 |
| child 29304 | 5c71a6da989d |
| 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 |
| 28228 | 8 |
imports Plain Code_Eval 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 |
|
| 27367 | 11 |
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
|
| 25964 | 12 |
|
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
13 |
end |