isabelle: src/HOL/Isar_examples/ROOT.ML@745f834281e2 (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	berghofe
	Wed, 18 Aug 1999 17:43:53 +0200
changeset 7260	745f834281e2
parent 6882	fe4e3d26fa8f
child 7384	33c976216121
permissions	-rw-r--r--