isabelle: src/HOL/Isar_examples/ROOT.ML@7d3136b9af08 (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";
6882 fe4e3d26fa8f added KnasterTarski.thy; wenzelm parents: 6765 diff changeset	14	use_thy "KnasterTarski";

author	paulson
	Thu, 26 Aug 1999 11:34:17 +0200
changeset 7360	7d3136b9af08
parent 6882	fe4e3d26fa8f
child 7384	33c976216121
permissions	-rw-r--r--