author | huffman |
Thu, 04 Dec 2008 16:05:45 -0800 | |
changeset 28987 | dc0ab579a5ca |
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 |