isabelle: src/HOL/ex/ROOT.ML@e8197c9f1b5c (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
24528 e8197c9f1b5c tuned; wenzelm parents: 24478 diff changeset	7	no_document use_thys [
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	8	"Parity",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	9	"GCD"
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	10	];
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	11
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	12	use_thys [
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	13	"Higher_Order_Logic",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	14	"Abstract_NAT",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	15	"Guess",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	16	"Binary",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	17	"Recdefs",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	18	"Fundefs",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	19	"InductiveInvariant_examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	20	"Locales",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	21	"LocaleTest2",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	22	"Records",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	23	"MonoidGroup",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	24	"BinEx",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	25	"Hex_Bin_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	26	"Antiquote",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	27	"Multiquote",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	28	"PER",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	29	"NatSum",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	30	"ThreeDivides",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	31	"Intuitionistic",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	32	"CTL",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	33	"Arith_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	34	"BT",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	35	"InSort",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	36	"Qsort",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	37	"MergeSort",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	38	"Puzzle",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	39	"Lagrange",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	40	"Groebner_Examples",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	41	"MT",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	42	"Unification",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	43	"Commutative_RingEx",
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	44	"Commutative_Ring_Complete"
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	45	];
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20866 diff changeset	46
19438 6d266e266b3f early test of Classpackage, Codegenerator; wenzelm parents: 19281 diff changeset	47	no_document time_use_thy "Classpackage";
23271 3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	48
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	49	no_document time_use_thy "Eval";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	50	time_use_thy "Eval_Examples";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	51
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	52	no_document time_use_thy "State_Monad";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	53	no_document time_use_thy "Pretty_Int";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	54	time_use_thy "Random";
3f9ef4bf3f31 tuned document; wenzelm parents: 23193 diff changeset	55
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23808 diff changeset	56	no_document time_use_thy "Executable_Rat";
688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23808 diff changeset	57	no_document time_use_thy "Efficient_Nat";
21911 e29bcab0c81c added OCaml code generation (without dictionaries) haftmann parents: 21256 diff changeset	58	no_document time_use_thy "Codegenerator";
24195 7d1a16c77f7c tuned haftmann parents: 24127 diff changeset	59	no_document time_use_thy "Codegenerator_Pretty";
19438 6d266e266b3f early test of Classpackage, Codegenerator; wenzelm parents: 19281 diff changeset	60
12360 9c156045c8f2 added Higher_Order_Logic.thy; wenzelm parents: 12276 diff changeset	61
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	62	setmp proofs 2 time_use_thy "Hilbert_Classical";
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	63
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	64	time_use_thy "Primrec";
24478 fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	65	time_use_thy "Classical";
fb5e3fcfc10c some simultaneous use_thys; wenzelm parents: 24195 diff changeset	66	time_use_thy "set";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	67
24127 a56b6ed2e49c converted Meson tests to proper theory; wenzelm parents: 23854 diff changeset	68	time_use_thy "Meson_Test";
23454 c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23302 diff changeset	69	time_use_thy "Dense_Linear_Order_Ex";
13880 4f7f30f68926 Added examples for Presburger arithmetic. berghofe parents: 13200 diff changeset	70	time_use_thy "PresburgerEx";
23808 4e4b92e76219 fixed SML/NJ int problem haftmann parents: 23502 diff changeset	71	time_use_thy "Reflected_Presburger";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	72
20325 ec52000deb44 added HOL/ex/Reflection; wenzelm parents: 19997 diff changeset	73	time_use_thy "Reflection";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	74
23502 cc726aa7d66a added NBE nipkow parents: 23454 diff changeset	75	time_use_thy "NBE";
cc726aa7d66a added NBE nipkow parents: 23454 diff changeset	76
14569 78b75a9eec01 Added ex/Exceptions.thy nipkow parents: 14494 diff changeset	77	no_document use_thy "FuncSet";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	78	time_use_thy "Tarski";
d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	79
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: 12450 diff changeset	80	time_use_thy "SVC_Oracle";
12115 d0d41884f787 back to normal; wenzelm parents: 12105 diff changeset	81	if_svc_enabled time_use_thy "svc_test";
14459 0a8619367a61 added Refute_Examples.thy webertj parents: 14244 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: *)
18678 dd0c569fa43d sane ERROR handling; wenzelm parents: 18408 diff changeset	85	try time_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
07da804d1119 ex/Sudoku.thy webertj parents: 17783 diff changeset	90	time_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
14462 e6550f190fe9 Refute_Examples added/fixed webertj parents: 14459 diff changeset	93	time_use_thy "Refute_Examples";
14592 dd1a2905ea73 Added theory with examples for quickcheck command. berghofe parents: 14569 diff changeset	94	time_use_thy "Quickcheck_Examples";
19832 1a09f25410da nbe -> NormalForm nipkow parents: 19438 diff changeset	95	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	96
14569 78b75a9eec01 Added ex/Exceptions.thy nipkow parents: 14494 diff changeset	97	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	98	time_use_thy "Adder";
14569 78b75a9eec01 Added ex/Exceptions.thy nipkow parents: 14494 diff changeset	99
17466 92d36be64b46 Hebrew: HTML.with_charset; wenzelm parents: 17413 diff changeset	100	HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
17505 928bd7053d6a Chinese Unicode example; wenzelm parents: 17466 diff changeset	101	HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";

author	wenzelm
	Wed, 05 Sep 2007 20:48:25 +0200
changeset 24528	e8197c9f1b5c
parent 24478	fb5e3fcfc10c
child 24530	1bac25879117
permissions	-rw-r--r--