isabelle: src/HOL/Isar_examples/ROOT.ML@6ca6b6bd6e15 (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	ID: $Id$
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	4
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	5	Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	6	*)
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	7
24228 9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	8	no_document use_thys ["../NumberTheory/Primes", "../NumberTheory/Fibonacci"];
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	9
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	10	use_thys [
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	11	"BasicLogic",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	12	"Cantor",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	13	"Peirce",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	14	"Drinker",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	15	"ExprCompiler",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	16	"Group",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	17	"Summation",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	18	"KnasterTarski",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	19	"MutilatedCheckerboard",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	20	"Puzzle",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	21	"NestedDatatype",
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	22	"HoareEx"
9e2234f2aff1 simultaneous use_thys; wenzelm parents: 19022 diff changeset	23	];

author	huffman
	Thu, 19 Feb 2009 12:03:31 -0800
changeset 29994	6ca6b6bd6e15
parent 24228	9e2234f2aff1
child 31758	3edd5f813f01
permissions	-rw-r--r--