src/HOL/Main.thy
author haftmann
Mon, 25 Oct 2010 13:34:57 +0200
changeset 40121 e7a80c6752c9
parent 38393 7c045c03598f
child 40178 00152d17855b
permissions -rw-r--r--
moved sledgehammer to Plain; tuned dependencies
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
40121
e7a80c6752c9 moved sledgehammer to Plain; tuned dependencies
haftmann
parents: 38393
diff changeset
     4
imports Plain Record Predicate_Compile Nitpick SMT Quotient
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