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

9000 c20d58286a51 cleaned up; wenzelm parents: 8944 diff changeset	1	(* Title: HOL/ex/ROOT.ML
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	3
9297 bafe45732b10 tuned; wenzelm parents: 9100 diff changeset	4	Miscellaneous examples for Higher-Order Logic.
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6
5753 c90b5f7d0c61 tuned; wenzelm parents: 5368 diff changeset	7	(some examples of recursive function definitions: the TFL package)
5124 1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5078 diff changeset	8	time_use_thy "Recdefs";
3337 c056d328aa0e Primrec: New example ported from ZF paulson parents: 3294 diff changeset	9	time_use_thy "Primrec";
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	10
11586 d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	11	setmp proofs 2 time_use_thy "Hilbert_Classical";
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	12
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	13	(advanced concrete syntax)
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	14	time_use_thy "Tuple";
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	15	time_use_thy "Antiquote";
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	16	time_use_thy "Multiquote";
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	17
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	18	(basic use of extensible records)
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	19	time_use_thy "MonoidGroup";
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	20	time_use_thy "Records";
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	21
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	22	time_use_thy "StringEx";
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	23	time_use_thy "BinEx";
d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	24
8944 96964d43a472 restored NatSum.thy paulson parents: 8933 diff changeset	25	time_use_thy "NatSum";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	26	time_use "cla.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	27	time_use "mesontest.ML";
10440 2074e62da354 proper theory context for mesontest2; wenzelm parents: 10052 diff changeset	28	time_use_thy "mesontest2";
1174 e57a93d41de0 added mention of new theories BT and Perm lcp parents: 1165 diff changeset	29	time_use_thy "BT";
8797 b55e2354d71e Added AVL nipkow parents: 8569 diff changeset	30	time_use_thy "AVL";
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	31	time_use_thy "InSort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	32	time_use_thy "Qsort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	33	time_use_thy "Puzzle";
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	34
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: 4809 diff changeset	35	time_use_thy "IntRing";
7b5ea59c0275 Installation of target HOL-Real paulson parents: 4809 diff changeset	36
9100 9e081c812338 fixed deps; wenzelm parents: 9000 diff changeset	37	time_use_thy "set";
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	38	time_use_thy "MT";
7085 e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller paulson parents: 6349 diff changeset	39	time_use_thy "Tarski";
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1174 diff changeset	40
7304 94c6f8f07631 if_svc_enabled; wenzelm parents: 7187 diff changeset	41	if_svc_enabled time_use_thy "svc_test";

author	wenzelm
	Fri, 05 Oct 2001 21:52:39 +0200
changeset 11701	3d51fbf81c17
parent 11586	d8a7f6318457
child 12080	4c1e3a2a87c3
permissions	-rw-r--r--