src/HOL/NumberTheory/ROOT.ML
author krauss
Mon, 12 May 2008 22:11:06 +0200
changeset 26875 e18574413bc4
parent 24104 719fbe4fb77f
permissions -rw-r--r--
Measure functions can now be declared via special rules, allowing for a prolog-style generation of measure functions for a specific type.

(* $Id$ *)

no_document use_thys ["Infinite_Set", "Permutation", "Primes"];
use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
  "WilsonBij", "Quadratic_Reciprocity"];