isabelle: src/HOL/ex/ROOT.ML@4dc132902672 (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
12360 9c156045c8f2 added Higher_Order_Logic.thy; wenzelm parents: 12276 diff changeset	7	time_use_thy "Higher_Order_Logic";
9c156045c8f2 added Higher_Order_Logic.thy; wenzelm parents: 12276 diff changeset	8
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	9	time_use_thy "Recdefs";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	10	time_use_thy "Primrec";
12276 7bafe3d6c248 time_use_thy "Locales"; wenzelm parents: 12274 diff changeset	11	time_use_thy "Locales";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	12	time_use_thy "Records";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	13	time_use_thy "MonoidGroup";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	14	time_use_thy "StringEx";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	15	time_use_thy "BinEx";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	16	setmp proofs 2 time_use_thy "Hilbert_Classical";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	17	time_use_thy "Antiquote";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	18	time_use_thy "Multiquote";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	19	time_use_thy "Tuple";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	20
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	21	time_use_thy "NatSum";
12450 1162b280700a Added example file for intuitionistic logic (taken from FOL). berghofe parents: 12360 diff changeset	22	time_use_thy "Intuitionistic";
14220 4dc132902672 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy paulson parents: 13880 diff changeset	23	time_use_thy "Classical";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	24	time_use_thy "mesontest2";
13880 4f7f30f68926 Added examples for Presburger arithmetic. berghofe parents: 13200 diff changeset	25	time_use_thy "PresburgerEx";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	26	time_use_thy "BT";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	27	time_use_thy "AVL";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	28	time_use_thy "InSort";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	29	time_use_thy "Qsort";
13200 7618f289c9c1 Added ex/MergeSort nipkow parents: 12869 diff changeset	30	time_use_thy "MergeSort";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	31	time_use_thy "Puzzle";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	32
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	33	time_use_thy "IntRing";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	34
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	35	time_use_thy "set";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	36	time_use_thy "MT";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	37	time_use_thy "Tarski";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	38
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: 12450 diff changeset	39	time_use_thy "SVC_Oracle";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	40	if_svc_enabled time_use_thy "svc_test";

author	paulson
	Wed, 08 Oct 2003 15:57:41 +0200
changeset 14220	4dc132902672
parent 13880	4f7f30f68926
child 14244	f58598341d30
permissions	-rw-r--r--