isabelle: src/HOL/ex/ROOT.ML@d0d41884f787 (annotated)

12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	1	(* Title: HOL/ex/ROOT.ML
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	2	ID: $Id$
11586 d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	3
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	4	Miscellaneous examples for Higher-Order Logic.
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	5	*)
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	6
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	7	time_use_thy "Recdefs";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	8	time_use_thy "Primrec";
12080 4c1e3a2a87c3 use_thy "Locales"; wenzelm parents: 11586 diff changeset	9	time_use_thy "Locales";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	10	time_use_thy "Records";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	11	time_use_thy "MonoidGroup";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	12	time_use_thy "StringEx";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	13	time_use_thy "BinEx";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	14	setmp proofs 2 time_use_thy "Hilbert_Classical";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	15	time_use_thy "Antiquote";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	16	time_use_thy "Multiquote";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	17	time_use_thy "Tuple";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	18
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	19	time_use_thy "NatSum";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	20	time_use "cla.ML";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	21	time_use "mesontest.ML";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	22	time_use_thy "mesontest2";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	23	time_use_thy "BT";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	24	time_use_thy "AVL";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	25	time_use_thy "InSort";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	26	time_use_thy "Qsort";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	27	time_use_thy "Puzzle";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	28
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	29	time_use_thy "IntRing";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	30
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	31	time_use_thy "set";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	32	time_use_thy "MT";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	33	time_use_thy "Tarski";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	34
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	35	if_svc_enabled time_use_thy "svc_test";

author	wenzelm
	Fri, 09 Nov 2001 00:11:52 +0100
changeset 12115	d0d41884f787
parent 12105	1e4451999200
child 12274	2582d16acd3d
permissions	-rw-r--r--