src/HOL/Isar_examples/ROOT.ML
author wenzelm
Tue, 27 Apr 1999 10:45:20 +0200
changeset 6516 09207771cc7c
parent 6444 2ebe9e630cab
child 6526 6b64d1454ee3
permissions -rw-r--r--
added Isar_examples/Cantor.ML;

(*  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";