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

12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	1	(* Title: HOL/ex/ROOT.ML
11586 d8a7f6318457 tuned; wenzelm parents: 11445 diff changeset	2
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	3	Miscellaneous examples for Higher-Order Logic.
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	4	*)
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	5
24528 e8197c9f1b5c tuned; wenzelm parents: 24478 diff changeset	6	no_document use_thys [
41413 64cd30d6b0b8 explicit file specifications -- avoid secondary load path; wenzelm parents: 40946 diff changeset	7	"~~/src/HOL/Library/State_Monad",
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	8	"Efficient_Nat_examples",
41413 64cd30d6b0b8 explicit file specifications -- avoid secondary load path; wenzelm parents: 40946 diff changeset	9	"~~/src/HOL/Library/FuncSet",
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	10	"Eval_Examples",
40946 3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 40632 diff changeset	11	"Normalization_by_Evaluation",
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 40632 diff changeset	12	"Hebrew",
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 40632 diff changeset	13	"Chinese",
43804 eb9be23db2b7 cleanly separate TPTP related files from other examples blanchet parents: 43242 diff changeset	14	"Serbian"
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	15	];
07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	16
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	17	use_thys [
40239 c4336e45f199 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; wenzelm parents: 39395 diff changeset	18	"Iff_Oracle",
40281 3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010). wenzelm parents: 40239 diff changeset	19	"Coercion_Examples",
46558 fdb84c40e074 renamed ex/Numeral.thy to ex/Numeral_Representation.thy huffman parents: 46395 diff changeset	20	"Numeral_Representation",
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	21	"Higher_Order_Logic",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	22	"Abstract_NAT",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	23	"Guess",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	24	"Binary",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	25	"Fundefs",
33471 5aef13872723 renamed method induct_scheme to induction_schema krauss parents: 33436 diff changeset	26	"Induction_Schema",
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	27	"LocaleTest2",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	28	"Records",
37760 8380686be5cd moved example to its own file in HOL/ex krauss parents: 37695 diff changeset	29	"While_Combinator_Example",
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	30	"MonoidGroup",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	31	"BinEx",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	32	"Hex_Bin_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	33	"Antiquote",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	34	"Multiquote",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	35	"PER",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	36	"NatSum",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	37	"ThreeDivides",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	38	"Intuitionistic",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	39	"CTL",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	40	"Arith_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	41	"BT",
33436 0b5f07dd68f5 New nipkow parents: 33356 diff changeset	42	"Tree23",
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	43	"MergeSort",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	44	"Lagrange",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	45	"Groebner_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	46	"MT",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	47	"Unification",
24740 36750aca7a77 some more simultaneous use_thys; wenzelm parents: 24615 diff changeset	48	"Primrec",
36750aca7a77 some more simultaneous use_thys; wenzelm parents: 24615 diff changeset	49	"Tarski",
25738 b091cbae3e2a included meson/metis tests in simultaneous use_thys; wenzelm parents: 25568 diff changeset	50	"Classical",
44276 fe769a0fcc96 avoid case-sensitive name for example theory haftmann parents: 44145 diff changeset	51	"Set_Theory",
27436 9581777503e9 code antiquotation roaring ahead haftmann parents: 27421 diff changeset	52	"Meson_Test",
29181 cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method krauss parents: 28952 diff changeset	53	"Termination",
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	54	"Coherent",
2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	55	"PresburgerEx",
29377 e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	56	"ReflectionEx",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	57	"Sqrt",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	58	"Sqrt_Script",
32560 c83dab2c5988 corrected upper/lowercase haftmann parents: 32556 diff changeset	59	"Transfer_Ex",
29377 e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	60	"Arithmetic_Series_Complex",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	61	"HarmonicSeries",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	62	"Refute_Examples",
29697 e8785144719d Added Formal_Power_Series_Examples to HOL-ex image chaieb parents: 29650 diff changeset	63	"Quickcheck_Examples",
37917 67ccea8a4761 added new theories to IsaMakefile and ROOT.ML bulwahn parents: 37760 diff changeset	64	"Quickcheck_Lattice_Examples",
35160 6eb2b6c1d2d5 a draft for an example how to turn specifications involving choice executable haftmann parents: 33651 diff changeset	65	"Landau",
35163 2e0966d6f951 added simple theory about discrete summation haftmann parents: 35160 diff changeset	66	"Execute_Choice",
35328 e8888458dce3 Moved old Integration to examples. hoelzl parents: 35163 diff changeset	67	"Summation",
36793 27da0a27b76f put construction of reals using Dedekind cuts in HOL/ex huffman parents: 35953 diff changeset	68	"Gauge_Integration",
40349 131cf8790a1c moved theory Quicksort from Library/ to ex/ haftmann parents: 40281 diff changeset	69	"Dedekind_Real",
40632 dc55e6752046 adding birthday paradoxon from some abandoned drawer bulwahn parents: 40349 diff changeset	70	"Quicksort",
43238 04c886a1d1a5 renaming the formalisation of the birthday problem to a proper English name bulwahn parents: 42607 diff changeset	71	"Birthday_Paradox",
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: 41465 diff changeset	72	"List_to_Set_Comprehension_Examples",
44962 5554ed48b13f finite sequences as useful as introductory example; wenzelm parents: 44276 diff changeset	73	"Set_Algebras",
45224 b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML huffman parents: 45038 diff changeset	74	"Seq",
46395 f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type bulwahn parents: 45224 diff changeset	75	"Simproc_Tests",
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type bulwahn parents: 45224 diff changeset	76	"Executable_Relation"
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	77	];
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20866 diff changeset	78
41952 c7297638599b cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection; wenzelm parents: 41932 diff changeset	79	if getenv "ISABELLE_GHC" = "" then ()
41932 e8f113ce8a94 adapting Quickcheck_Narrowing and example file to new names bulwahn parents: 41914 diff changeset	80	else use_thy "Quickcheck_Narrowing_Examples";
41914 4ef7e6e317fa only testing theory LSC_Examples when GHC is installed on the machine bulwahn parents: 41911 diff changeset	81
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	82	use_thy "SVC_Oracle";
32428 700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably; wenzelm parents: 32259 diff changeset	83	if getenv "SVC_HOME" = "" then ()
700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably; wenzelm parents: 32259 diff changeset	84	else use_thy "svc_test";
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	85
32428 700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably; wenzelm parents: 32259 diff changeset	86	(requires zChaff (or some other reasonably fast SAT solver))
700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably; wenzelm parents: 32259 diff changeset	87	if getenv "ZCHAFF_HOME" = "" then ()
700ed1f4c576 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably; wenzelm parents: 32259 diff changeset	88	else use_thy "Sudoku";
18408 07da804d1119 ex/Sudoku.thy webertj parents: 17783 diff changeset	89
33546 5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects; wenzelm parents: 33471 diff changeset	90	(requires a proof-generating SAT solver (zChaff or MiniSAT))
5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects; wenzelm parents: 33471 diff changeset	91	(global side-effects ahead!)
5e2d381b0695 try SAT_Examples last, to minimize impact of global side-effects; wenzelm parents: 33471 diff changeset	92	try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)

author	huffman
	Tue, 21 Feb 2012 09:17:53 +0100
changeset 46558	fdb84c40e074
parent 46395	f56be74d7f51
child 46585	f462e49eaf11
permissions	-rw-r--r--