isabelle: src/HOL/Isar_examples/ROOT.ML@15d6c121d75f (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
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	8	use_thy "BasicLogic";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	9	use_thy "Peirce";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	10	use_thy "Cantor";
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	11	use_thy "ExprCompiler";
6765 6eba3d69037b added Group.thy; wenzelm parents: 6559 diff changeset	12	use_thy "Group";
6526 6b64d1454ee3 added Isar_examples/NatSum.thy; wenzelm parents: 6444 diff changeset	13	use_thy "NatSum";

author	paulson
	Thu, 17 Jun 1999 10:35:01 +0200
changeset 6833	15d6c121d75f
parent 6765	6eba3d69037b
child 6882	fe4e3d26fa8f
permissions	-rw-r--r--