src/HOL/Isar_examples/ROOT.ML
author nipkow
Tue, 07 Jul 2009 17:39:51 +0200
changeset 31952 40501bb2d57c
parent 31758 3edd5f813f01
child 32479 521cc9bf2958
permissions -rw-r--r--
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int

(*  Title:      HOL/Isar_examples/ROOT.ML
    Author:     Markus Wenzel, TU Muenchen

Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
*)

no_document use_thys ["../NumberTheory/Primes", "../NumberTheory/Fibonacci"];

use_thys [
  "Basic_Logic",
  "Cantor",
  "Peirce",
  "Drinker",
  "Expr_Compiler",
  "Group",
  "Summation",
  "Knaster_Tarski",
  "Mutilated_Checkerboard",
  "Puzzle",
  "Nested_Datatype",
  "Hoare_Ex"
];