isabelle: src/HOL/ex/ROOT.ML@e28b41e8b7d4 (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
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20866 diff changeset	7	no_document use_thy "Parity";
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20866 diff changeset	8	no_document use_thy "GCD";
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20866 diff changeset	9
19438 6d266e266b3f early test of Classpackage, Codegenerator; wenzelm parents: 19281 diff changeset	10	no_document time_use_thy "Classpackage";
23271 3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	11
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	12	no_document time_use_thy "Eval";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	13	time_use_thy "Eval_Examples";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	14
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	15	no_document time_use_thy "State_Monad";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	16	no_document time_use_thy "Pretty_Int";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	17	time_use_thy "Random";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	18
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	19	no_document time_use_thy "ExecutableRat";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	20	no_document time_use_thy "EfficientNat";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	21	time_use_thy "Codegenerator_Rat";
21911 e29bcab0c81c added OCaml code generation (without dictionaries) haftmann parents: 21256 diff changeset	22	no_document time_use_thy "Codegenerator";
19438 6d266e266b3f early test of Classpackage, Codegenerator; wenzelm parents: 19281 diff changeset	23
12360 9c156045c8f2 added Higher_Order_Logic.thy; wenzelm parents: 12276 diff changeset	24	time_use_thy "Higher_Order_Logic";
19085 a1a251b297dd added ex/Abstract_NAT.thy; wenzelm parents: 19022 diff changeset	25	time_use_thy "Abstract_NAT";
19997 fe69952f09f6 added ex/Guess.thy; wenzelm parents: 19832 diff changeset	26	time_use_thy "Guess";
22140 0d49078c28bd added HOL/ex/Binary.thy; wenzelm parents: 22067 diff changeset	27	time_use_thy "Binary";
12360 9c156045c8f2 added Higher_Order_Logic.thy; wenzelm parents: 12276 diff changeset	28
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	29	time_use_thy "Recdefs";
22167 c3afded569ea Included ex/Fundefs.thy in HOL-ex session krauss parents: 22140 diff changeset	30	time_use_thy "Fundefs";
14244 f58598341d30 InductiveInvariant_examples illustrates advanced recursive function definitions paulson parents: 14220 diff changeset	31	time_use_thy "InductiveInvariant_examples";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	32	time_use_thy "Primrec";
12276 7bafe3d6c248 time_use_thy "Locales"; wenzelm parents: 12274 diff changeset	33	time_use_thy "Locales";
22657 731622340817 New file for locale regression tests. ballarin parents: 22528 diff changeset	34	time_use_thy "LocaleTest2";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	35	time_use_thy "Records";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	36	time_use_thy "MonoidGroup";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	37	time_use_thy "BinEx";
20866 bc366b4b6ea4 examples for hex and bin numerals kleing parents: 20812 diff changeset	38	time_use_thy "Hex_Bin_Examples";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	39	setmp proofs 2 time_use_thy "Hilbert_Classical";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	40	time_use_thy "Antiquote";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	41	time_use_thy "Multiquote";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	42
20812 cc6b31c2b9a2 reactivated theory PER; wenzelm parents: 20597 diff changeset	43	time_use_thy "PER";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	44	time_use_thy "NatSum";
19022 0e6ec4fd204c * moved ThreeDivides from Isar_examples to better suited HOL/ex kleing parents: 18678 diff changeset	45	time_use_thy "ThreeDivides";
12450 1162b280700a Added example file for intuitionistic logic (taken from FOL). berghofe parents: 12360 diff changeset	46	time_use_thy "Intuitionistic";
14220 4dc132902672 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy paulson parents: 13880 diff changeset	47	time_use_thy "Classical";
15871 e524119dbf19 * empty log message * bauerg parents: 15037 diff changeset	48	time_use_thy "CTL";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	49	time_use_thy "mesontest2";
23193 1f2d94b6a8ef some tests for arith added webertj parents: 23191 diff changeset	50	time_use_thy "Arith_Examples";
23454 c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23302 diff changeset	51	time_use_thy "Dense_Linear_Order_Ex";
13880 4f7f30f68926 Added examples for Presburger arithmetic. berghofe parents: 13200 diff changeset	52	time_use_thy "PresburgerEx";
23302 919d5c1fe509 disabled theory "Reflected_Presburger" for smlnj (temporarily); wenzelm parents: 23271 diff changeset	53	if String.isPrefix "smlnj" ml_system then () (* FIXME tmp *)
919d5c1fe509 disabled theory "Reflected_Presburger" for smlnj (temporarily); wenzelm parents: 23271 diff changeset	54	else time_use_thy "Reflected_Presburger";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	55	time_use_thy "BT";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	56	time_use_thy "InSort";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	57	time_use_thy "Qsort";
13200 7618f289c9c1 Added ex/MergeSort nipkow parents: 12869 diff changeset	58	time_use_thy "MergeSort";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	59	time_use_thy "Puzzle";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	60
14603 985eb6708207 Moved ring stuff from ex into Ring_and_Field. nipkow parents: 14592 diff changeset	61	time_use_thy "Lagrange";
23271 3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	62	time_use_thy "Groebner_Examples";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	63
17378 105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy chaieb parents: 15871 diff changeset	64	time_use_thy "Commutative_RingEx";
105519771c67 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy chaieb parents: 15871 diff changeset	65	time_use_thy "Commutative_Ring_Complete";
20325 ec52000deb44 added HOL/ex/Reflection; wenzelm parents: 19997 diff changeset	66	time_use_thy "Reflection";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	67
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	68	time_use_thy "set";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	69	time_use_thy "MT";
14569 78b75a9eec01 Added ex/Exceptions.thy nipkow parents: 14494 diff changeset	70
78b75a9eec01 Added ex/Exceptions.thy nipkow parents: 14494 diff changeset	71	no_document use_thy "FuncSet";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	72	time_use_thy "Tarski";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	73
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: 12450 diff changeset	74	time_use_thy "SVC_Oracle";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	75	if_svc_enabled time_use_thy "svc_test";
14459 0a8619367a61 added Refute_Examples.thy webertj parents: 14244 diff changeset	76
23191 b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	77	(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	78	(* installed: *)
18678 dd0c569fa43d sane ERROR handling; wenzelm parents: 18408 diff changeset	79	try time_use_thy "SAT_Examples";
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: 17505 diff changeset	80
23191 b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	81	(* requires zChaff (or some other reasonably fast SAT solver) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	82	(* installed: *)
18408 07da804d1119 ex/Sudoku.thy webertj parents: 17783 diff changeset	83	if getenv "ZCHAFF_HOME" <> "" then
07da804d1119 ex/Sudoku.thy webertj parents: 17783 diff changeset	84	time_use_thy "Sudoku"
23191 b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	85	else ();
18408 07da804d1119 ex/Sudoku.thy webertj parents: 17783 diff changeset	86
14462 e6550f190fe9 Refute_Examples added/fixed webertj parents: 14459 diff changeset	87	time_use_thy "Refute_Examples";
14592 dd1a2905ea73 Added theory with examples for quickcheck command. berghofe parents: 14569 diff changeset	88	time_use_thy "Quickcheck_Examples";
19832 1a09f25410da nbe -> NormalForm nipkow parents: 19438 diff changeset	89	no_document time_use_thy "NormalForm";
14494 48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder) skalberg parents: 14482 diff changeset	90
14569 78b75a9eec01 Added ex/Exceptions.thy nipkow parents: 14494 diff changeset	91	no_document use_thy "Word";
14494 48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder) skalberg parents: 14482 diff changeset	92	time_use_thy "Adder";
14569 78b75a9eec01 Added ex/Exceptions.thy nipkow parents: 14494 diff changeset	93
17466 92d36be64b46 Hebrew: HTML.with_charset; wenzelm parents: 17413 diff changeset	94	HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
17505 928bd7053d6a Chinese Unicode example; wenzelm parents: 17466 diff changeset	95	HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
22999 c1ce129e6f9c Added unification case study (using new function package) krauss parents: 22657 diff changeset	96
c1ce129e6f9c Added unification case study (using new function package) krauss parents: 22657 diff changeset	97	time_use_thy "Unification";

author	huffman
	Thu, 21 Jun 2007 23:28:44 +0200
changeset 23470	e28b41e8b7d4
parent 23454	c54975167be9
child 23502	cc726aa7d66a
permissions	-rw-r--r--