isabelle: src/HOL/Isar_Examples/ROOT.ML@463daacae6c2 (annotated)

33026 8f35633c4922 modernized session Isar_Examples; wenzelm parents: 32479 diff changeset	1	(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
6444 2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	2
46582 dcc312f22ee8 misc tuning; wenzelm parents: 37672 diff changeset	3	no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"];
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	4
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	5	use_thys [
31758 3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	6	"Basic_Logic",
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	7	"Cantor",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	8	"Drinker",
31758 3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	9	"Expr_Compiler",
47871 861dc9184920 more accurate ROOT.ML; wenzelm parents: 46582 diff changeset	10	"Fibonacci",
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	11	"Group",
47871 861dc9184920 more accurate ROOT.ML; wenzelm parents: 46582 diff changeset	12	"Group_Context",
861dc9184920 more accurate ROOT.ML; wenzelm parents: 46582 diff changeset	13	"Group_Notepad",
861dc9184920 more accurate ROOT.ML; wenzelm parents: 46582 diff changeset	14	"Hoare_Ex",
31758 3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	15	"Knaster_Tarski",
3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	16	"Mutilated_Checkerboard",
47871 861dc9184920 more accurate ROOT.ML; wenzelm parents: 46582 diff changeset	17	"Nested_Datatype",
861dc9184920 more accurate ROOT.ML; wenzelm parents: 46582 diff changeset	18	"Peirce",
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	19	"Puzzle",
47871 861dc9184920 more accurate ROOT.ML; wenzelm parents: 46582 diff changeset	20	"Summation"
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	21	];

author	wenzelm
	Sun, 05 Aug 2012 13:23:54 +0200
changeset 48680	463daacae6c2
parent 47871	861dc9184920
permissions	-rw-r--r--