src/HOL/Main.thy
author paulson
Thu, 27 Sep 2007 17:55:28 +0200
changeset 24742 73b8b42a36b6
parent 24699 c6674504103f
child 25223 7463251e7273
permissions -rw-r--r--
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17602
63367feba417 header (title/ID) added
webertj
parents: 17601
diff changeset
     1
(*  Title:      HOL/Main.thy
63367feba417 header (title/ID) added
webertj
parents: 17601
diff changeset
     2
    ID:         $Id$
63367feba417 header (title/ID) added
webertj
parents: 17601
diff changeset
     3
*)
9619
6125cc9efc18 fixed deps;
wenzelm
parents: 9447
diff changeset
     4
12024
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     5
header {* Main HOL *}
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     6
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     7
theory Main
24699
c6674504103f datatype interpretators for size and datatype_realizer
haftmann
parents: 24644
diff changeset
     8
imports Map
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     9
begin
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    10
12024
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    11
text {*
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    12
  Theory @{text Main} includes everything.  Note that theory @{text
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    13
  PreList} already includes most HOL theories.
19608
81fe44909dd5 revert accidental text change;
wenzelm
parents: 19607
diff changeset
    14
*}
17395
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents: 17386
diff changeset
    15
23165
5d319b0f8bf9 HOL_proofs;
wenzelm
parents: 22840
diff changeset
    16
ML {* val HOL_proofs = !proofs *}
5d319b0f8bf9 HOL_proofs;
wenzelm
parents: 22840
diff changeset
    17
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    18
end