(* Title: HOL/Isar_examples/ROOT.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *) use_thy "BasicLogic"; use_thy "Peirce"; use_thy "Cantor"; use_thy "ExprCompiler"; use_thy "Group"; use_thy "NatSum"; use_thy "KnasterTarski";