isabelle: src/HOL/Isar_examples/ROOT.ML@8185d3bfcbf1 (annotated)

6444 2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	1	(* Title: HOL/Isar_examples/ROOT.ML
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	2	Author: Markus Wenzel, TU Muenchen
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	3
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	4	Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	5	*)
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	6
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	7	no_document use_thys ["../NumberTheory/Primes", "../NumberTheory/Fibonacci"];
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	8
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	9	use_thys [
31758 3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	10	"Basic_Logic",
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	11	"Cantor",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	12	"Peirce",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	13	"Drinker",
31758 3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	14	"Expr_Compiler",
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	15	"Group",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	16	"Summation",
31758 3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	17	"Knaster_Tarski",
3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	18	"Mutilated_Checkerboard",
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	19	"Puzzle",
31758 3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	20	"Nested_Datatype",
3edd5f813f01 observe standard theory naming conventions; wenzelm parents: 24228 diff changeset	21	"Hoare_Ex"
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	22	];

author	wenzelm
	Tue, 04 Aug 2009 15:59:57 +0200
changeset 32323	8185d3bfcbf1
parent 31758	3edd5f813f01
child 32479	521cc9bf2958
permissions	-rw-r--r--