isabelle: src/HOL/ex/ROOT.ML@d3b020134006 (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 [
24740 36750aca7a77 some more simultaneous use_thys; wenzelm parents: 24615 diff changeset	7	"State_Monad",
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	8	"Efficient_Nat_examples",
07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	9	"FuncSet",
07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	10	"Word",
07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	11	"Eval_Examples",
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 31181 diff changeset	12	"Codegenerator_Test",
d1cbf6393964 tuned code generator test theories haftmann parents: 31181 diff changeset	13	"Codegenerator_Pretty_Test",
29377 e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	14	"NormalForm",
30374 7311a1546d85 added predicate compiler, as formally checked prototype, not as user package haftmann parents: 30179 diff changeset	15	"../NumberTheory/Factorization",
31129 d2cead76fca2 split Predicate_Compile examples into separate theory haftmann parents: 30740 diff changeset	16	"Predicate_Compile",
d2cead76fca2 split Predicate_Compile examples into separate theory haftmann parents: 30740 diff changeset	17	"Predicate_Compile_ex"
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	18	];
07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25738 diff changeset	19
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	20	use_thys [
28021 32acf3c6cd12 added HOL/ex/Numeral.thy haftmann parents: 27742 diff changeset	21	"Numeral",
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	22	"Higher_Order_Logic",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	23	"Abstract_NAT",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	24	"Guess",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	25	"Binary",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	26	"Recdefs",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	27	"Fundefs",
25568 7bb10db582cf Adding "ex/Induction_Scheme.thy" to tests krauss parents: 25543 diff changeset	28	"Induction_Scheme",
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	29	"InductiveInvariant_examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	30	"LocaleTest2",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	31	"Records",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	32	"MonoidGroup",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	33	"BinEx",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	34	"Hex_Bin_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	35	"Antiquote",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	36	"Multiquote",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	37	"PER",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	38	"NatSum",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	39	"ThreeDivides",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	40	"Intuitionistic",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	41	"CTL",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	42	"Arith_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	43	"BT",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	44	"MergeSort",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	45	"Lagrange",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	46	"Groebner_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	47	"MT",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	48	"Unification",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	49	"Commutative_RingEx",
24740 36750aca7a77 some more simultaneous use_thys; wenzelm parents: 24615 diff changeset	50	"Commutative_Ring_Complete",
36750aca7a77 some more simultaneous use_thys; wenzelm parents: 24615 diff changeset	51	"Primrec",
36750aca7a77 some more simultaneous use_thys; wenzelm parents: 24615 diff changeset	52	"Tarski",
25738 b091cbae3e2a included meson/metis tests in simultaneous use_thys; wenzelm parents: 25568 diff changeset	53	"Adder",
b091cbae3e2a included meson/metis tests in simultaneous use_thys; wenzelm parents: 25568 diff changeset	54	"Classical",
b091cbae3e2a included meson/metis tests in simultaneous use_thys; wenzelm parents: 25568 diff changeset	55	"set",
27436 9581777503e9 code antiquotation roaring ahead haftmann parents: 27421 diff changeset	56	"Meson_Test",
29181 cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method krauss parents: 28952 diff changeset	57	"Termination",
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	58	"Coherent",
2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	59	"PresburgerEx",
29377 e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	60	"ReflectionEx",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	61	"BinEx",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	62	"Sqrt",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	63	"Sqrt_Script",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	64	"Arithmetic_Series_Complex",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	65	"HarmonicSeries",
e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	66	"Refute_Examples",
29697 e8785144719d Added Formal_Power_Series_Examples to HOL-ex image chaieb parents: 29650 diff changeset	67	"Quickcheck_Examples",
31381 b3a785a69538 added Landau theory haftmann parents: 31378 diff changeset	68	"Formal_Power_Series_Examples",
b3a785a69538 added Landau theory haftmann parents: 31378 diff changeset	69	"Landau"
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	70	];
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20866 diff changeset	71
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	72	setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	73
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	74
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	75	use_thy "SVC_Oracle";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	76
28263 69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 28243 diff changeset	77	fun svc_enabled () = getenv "SVC_HOME" <> "";
69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 28243 diff changeset	78	fun if_svc_enabled f x = if svc_enabled () then f x else ();
69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 28243 diff changeset	79
29377 e6439dbfeee1 more parallel loading; wenzelm parents: 29376 diff changeset	80	if_svc_enabled use_thy "svc_test";
14459 0a8619367a61 added Refute_Examples.thy webertj parents: 14244 diff changeset	81
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	82
23191 b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	83	(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	84	(* installed: *)
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	85	try use_thy "SAT_Examples";
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: 17505 diff changeset	86
23191 b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	87	(* requires zChaff (or some other reasonably fast SAT solver) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	88	(* installed: *)
18408 07da804d1119 ex/Sudoku.thy webertj parents: 17783 diff changeset	89	if getenv "ZCHAFF_HOME" <> "" then
29376 2071939cf0fc more parallel loading; wenzelm parents: 29181 diff changeset	90	use_thy "Sudoku"
23191 b7f3a30f3d7f MiniSAT mentioned in comment webertj parents: 22999 diff changeset	91	else ();
18408 07da804d1119 ex/Sudoku.thy webertj parents: 17783 diff changeset	92
30179 c703c9368c12 A Serbian theory, by Filip Maric. wenzelm parents: 29808 diff changeset	93	HTML.with_charset "utf-8" (no_document use_thys)
c703c9368c12 A Serbian theory, by Filip Maric. wenzelm parents: 29808 diff changeset	94	["Hebrew", "Chinese", "Serbian"];

author	paulson
	Wed, 01 Jul 2009 16:19:44 +0100
changeset 31909	d3b020134006
parent 31613	78ac5c304db7
child 32108	77094a0bbc3e
permissions	-rw-r--r--