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

10519 ade64af4c57c hide many names from Datatype_Universe. nipkow parents: 10386 diff changeset	1	(* Title: HOL/Main.thy
ade64af4c57c hide many names from Datatype_Universe. nipkow parents: 10386 diff changeset	2	ID: $Id$
ade64af4c57c hide many names from Datatype_Universe. nipkow parents: 10386 diff changeset	3	Author: Tobias Nipkow
ade64af4c57c hide many names from Datatype_Universe. nipkow parents: 10386 diff changeset	4	Copyright 2000 TU Muenchen
9619 6125cc9efc18 fixed deps; wenzelm parents: 9447 diff changeset	5
10519 ade64af4c57c hide many names from Datatype_Universe. nipkow parents: 10386 diff changeset	6	Theory Main includes everything.
ade64af4c57c hide many names from Datatype_Universe. nipkow parents: 10386 diff changeset	7	Note that theory PreList already includes most HOL theories.
ade64af4c57c hide many names from Datatype_Universe. nipkow parents: 10386 diff changeset	8	*)
9619 6125cc9efc18 fixed deps; wenzelm parents: 9447 diff changeset	9
11483 f4d10044a2cd Hilbert_Choice is needed only in Main itself paulson parents: 10519 diff changeset	10	theory Main = Map + String + Hilbert_Choice:
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	11
10261 bb2f1e859177 tuned declarations; wenzelm parents: 9876 diff changeset	12	(belongs to theory List)
bb2f1e859177 tuned declarations; wenzelm parents: 9876 diff changeset	13	declare lists_mono [mono]
bb2f1e859177 tuned declarations; wenzelm parents: 9876 diff changeset	14	declare map_cong [recdef_cong]
10386 581a5a143994 provide case names for rev_induct, rev_cases; wenzelm parents: 10261 diff changeset	15	lemmas rev_induct [case_names Nil snoc] = rev_induct
581a5a143994 provide case names for rev_induct, rev_cases; wenzelm parents: 10261 diff changeset	16	and rev_cases [case_names Nil snoc] = rev_exhaust
9768 a589b1d75b7b lemmas [mono] = lists_mono; wenzelm parents: 9650 diff changeset	17
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	18	end

author	paulson
	Wed, 08 Aug 2001 14:52:10 +0200
changeset 11483	f4d10044a2cd
parent 10519	ade64af4c57c
child 11533	0c0d2332e8f0
permissions	-rw-r--r--