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

1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: HOL/ex/ROOT
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4	Copyright 1991 University of Cambridge
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6	Executes miscellaneous examples for Higher-Order Logic.
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8
6349 f7750d816c21 removed foo_build_completed -- now handled by session management (via usedir); wenzelm parents: 5866 diff changeset	9	writeln "Root file for HOL examples";
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	10
4449 df30e75f670f tuned; wenzelm parents: 3404 diff changeset	11	set proof_timing;
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	12
5753 c90b5f7d0c61 tuned; wenzelm parents: 5368 diff changeset	13	(some examples of recursive function definitions: the TFL package)
5124 1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5078 diff changeset	14	time_use_thy "Recdefs";
4809 595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n) paulson parents: 4449 diff changeset	15	time_use_thy "Primes";
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	16	time_use_thy "Fib";
8353 57a163920480 new theory ex/Factorization paulson parents: 7304 diff changeset	17	with_path "../Induct" use_thy "Factorization";
3337 c056d328aa0e Primrec: New example ported from ZF paulson parents: 3294 diff changeset	18	time_use_thy "Primrec";
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	19
4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	20	time_use_thy "NatSum";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	21	time_use "cla.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	22	time_use "meson.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	23	time_use "mesontest.ML";
8557 fe75fe482566 restored the MESON examples file HOL/ex/mesontest2.ML paulson parents: 8353 diff changeset	24	time_use "mesontest2.ML";
1174 e57a93d41de0 added mention of new theories BT and Perm lcp parents: 1165 diff changeset	25	time_use_thy "BT";
8797 b55e2354d71e Added AVL nipkow parents: 8569 diff changeset	26	time_use_thy "AVL";
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	27	time_use_thy "InSort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	28	time_use_thy "Qsort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	29	time_use_thy "Puzzle";
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	30
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: 4809 diff changeset	31	time_use_thy "IntRing";
7b5ea59c0275 Installation of target HOL-Real paulson parents: 4809 diff changeset	32
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	33	time_use "set.ML";
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	34	time_use_thy "MT";
7085 e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller paulson parents: 6349 diff changeset	35	time_use_thy "Tarski";
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1174 diff changeset	36
5199 be986f7a6def added ex/MonoidGroups (record example); wenzelm parents: 5124 diff changeset	37	time_use_thy "StringEx";
be986f7a6def added ex/MonoidGroups (record example); wenzelm parents: 5124 diff changeset	38	time_use_thy "BinEx";
7187 676027b1d770 svc_enabled is now declared as a function paulson parents: 7180 diff changeset	39
7304 94c6f8f07631 if_svc_enabled; wenzelm parents: 7187 diff changeset	40	if_svc_enabled time_use_thy "svc_test";
5199 be986f7a6def added ex/MonoidGroups (record example); wenzelm parents: 5124 diff changeset	41
5753 c90b5f7d0c61 tuned; wenzelm parents: 5368 diff changeset	42	(basic use of extensible records)
5199 be986f7a6def added ex/MonoidGroups (record example); wenzelm parents: 5124 diff changeset	43	time_use_thy "MonoidGroup";
5753 c90b5f7d0c61 tuned; wenzelm parents: 5368 diff changeset	44	time_use_thy "Points";
5199 be986f7a6def added ex/MonoidGroups (record example); wenzelm parents: 5124 diff changeset	45
5753 c90b5f7d0c61 tuned; wenzelm parents: 5368 diff changeset	46	(groups via locales)
5250 1bff4b1e5ba9 added LocaleGroup, PiSets examples; wenzelm parents: 5199 diff changeset	47	time_use_thy "PiSets";
1bff4b1e5ba9 added LocaleGroup, PiSets examples; wenzelm parents: 5199 diff changeset	48	time_use_thy "LocaleGroup";
1bff4b1e5ba9 added LocaleGroup, PiSets examples; wenzelm parents: 5199 diff changeset	49
5753 c90b5f7d0c61 tuned; wenzelm parents: 5368 diff changeset	50	(expressions with quote / antiquote syntax)
5368 7c8d1c7c876d added Antiquote example; wenzelm parents: 5250 diff changeset	51	time_use_thy "Antiquote";
8569 748a9699f28d added HOL/ex/Multiquote.thy; wenzelm parents: 8557 diff changeset	52	time_use_thy "Multiquote";
5368 7c8d1c7c876d added Antiquote example; wenzelm parents: 5250 diff changeset	53
5199 be986f7a6def added ex/MonoidGroups (record example); wenzelm parents: 5124 diff changeset	54
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1026 diff changeset	55	writeln "END: Root file for HOL examples";

author	nipkow
	Fri, 05 May 2000 12:51:33 +0200
changeset 8797	b55e2354d71e
parent 8569	748a9699f28d
child 8933	de96f2982d2c
permissions	-rw-r--r--