src/HOL/Isar_examples/ROOT.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10257 21055ac27708
child 12105 1e4451999200
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/Isar_examples/ROOT.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
     6 *)
     7 
     8 time_use_thy "BasicLogic";
     9 time_use_thy "Cantor";
    10 time_use_thy "Peirce";
    11 time_use_thy "ExprCompiler";
    12 time_use_thy "Group";
    13 time_use_thy "Summation";
    14 time_use_thy "KnasterTarski";
    15 time_use_thy "MutilatedCheckerboard";
    16 with_path "../W0"           time_use_thy "W_correct";
    17 with_path "../NumberTheory" time_use_thy "Fibonacci";
    18 time_use_thy "Puzzle";
    19 time_use_thy "NestedDatatype";
    20 time_use_thy "HoareEx";