src/HOL/Main.thy
author bulwahn
Mon, 08 Nov 2010 09:25:43 +0100
changeset 40420 552563ea3304
parent 40181 3788b7adab36
child 41919 e180c2a9873b
permissions -rw-r--r--
adding code and theory for smallvalue generators, but do not setup the interpretation yet
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
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents: 40181
diff changeset
     4
imports Plain Record Predicate_Compile Smallcheck 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