src/HOL/Isar_examples/ROOT.ML

add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1

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

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

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

use_thys [
  "BasicLogic",
  "Cantor",
  "Peirce",
  "Drinker",
  "ExprCompiler",
  "Group",
  "Summation",
  "KnasterTarski",
  "MutilatedCheckerboard",
  "Puzzle",
  "NestedDatatype",
  "HoareEx"
];