isabelle: src/HOL/Main.thy@ade64af4c57c (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
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	10	theory Main = Map + String:
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	nipkow
	Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519	ade64af4c57c
parent 10386	581a5a143994
child 11483	f4d10044a2cd
permissions	-rw-r--r--