src/HOL/Algebra/ROOT.ML
author ballarin
Tue, 16 Dec 2008 21:10:53 +0100
changeset 29237 e90d9d51106b
parent 27713 95b36bfe7fc4
child 32480 6c19da8e661a
permissions -rw-r--r--
More porting to new locales.

(*
    The Isabelle Algebraic Library
    $Id$
    Author: Clemens Ballarin, started 24 September 1999
*)

(* Preliminaries from set and number theory *)
no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"];


(*** New development, based on explicit structures ***)

use_thys [
  (* Groups *)
  "FiniteProduct",      (* Product operator for commutative groups *)
  "Sylow",              (* Sylow's theorem *)
  "Bij",                (* Automorphism Groups *)

  (* Rings *)
  "Divisibility",       (* Rings *)
  "IntRing",            (* Ideals and residue classes *)
  "UnivPoly"            (* Polynomials *)
];


(*** Old development, based on axiomatic type classes.
     Will be withdrawn in future. ***)

no_document use_thys [
  "abstract/Abstract",  (*The ring theory*)
  "poly/Polynomial"     (*The full theory*)
];