src/HOL/Main.thy
author hoelzl
Mon, 03 Dec 2012 18:19:08 +0100
changeset 50328 25b1e8686ce0
parent 46155 f27cf421500a
child 51112 da97167e03f7
permissions -rw-r--r--
tuned proof
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
46155
f27cf421500a dropped theory More_Set
haftmann
parents: 45990
diff changeset
     4
imports Plain Predicate_Compile Nitpick
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