src/HOL/Main.thy
author wenzelm
Tue, 03 Mar 2009 14:07:43 +0100
changeset 30211 556d1810cdad
parent 29888 ab97183f1694
child 31203 5c8fb4fd67e0
permissions -rw-r--r--
Thm.binding;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12024
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     1
header {* Main HOL *}
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     2
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     3
theory Main
29888
ab97183f1694 Moved Nat_Int_Bij into Library
nipkow
parents: 29820
diff changeset
     4
imports Plain Code_Eval Map Recdef SAT
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     5
begin
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
     6
29304
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
     7
text {*
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
     8
  Classical Higher-order Logic -- only ``Main'', excluding real and
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
     9
  complex numbers etc.
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
    10
*}
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 28263
diff changeset
    11
27367
a75d71c73362 added dummy citiation
haftmann
parents: 26729
diff changeset
    12
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
25964
080f89d89990 consistent interacitve bootstrap of HOL-Main
haftmann
parents: 25223
diff changeset
    13
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    14
end