src/HOL/Algebra/ROOT.ML
author nipkow
Fri, 13 Nov 2009 14:14:04 +0100
changeset 33657 a4179bf442d1
parent 32480 6c19da8e661a
child 35849 b5522b51cb1e
permissions -rw-r--r--
renamed lemmas "anti_sym" -> "antisym"

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

(* Preliminaries from set and number theory *)
no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/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*)
];