isabelle: src/HOL/Main.thy@3130d7b3149d (annotated)

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
28091 50f2d6ba024c Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and nipkow parents: 27367 diff changeset	8	imports Plain Map Nat_Int_Bij Recdef
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
25223 7463251e7273 qualified Proofterm.proofs; wenzelm parents: 24742 diff changeset	11	ML {* val HOL_proofs = ! Proofterm.proofs *}
23165 5d319b0f8bf9 HOL_proofs; wenzelm parents: 22840 diff changeset	12
27367 a75d71c73362 added dummy citiation haftmann parents: 26729 diff changeset	13	text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
25964 080f89d89990 consistent interacitve bootstrap of HOL-Main haftmann parents: 25223 diff changeset	14
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	15	end

author	huffman
	Thu, 04 Sep 2008 17:19:57 +0200
changeset 28131	3130d7b3149d
parent 28091	50f2d6ba024c
child 28228	7ebe8dc06cbb
permissions	-rw-r--r--