src/HOL/Algebra/ROOT.ML
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 35849 b5522b51cb1e
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (*  Author: Clemens Ballarin, started 24 September 1999
     2 
     3 The Isabelle Algebraic Library.
     4 *)
     5 
     6 (* Preliminaries from set and number theory *)
     7 no_document use_thys [
     8   "~~/src/HOL/Library/FuncSet",
     9   "~~/src/HOL/Old_Number_Theory/Primes",
    10   "~~/src/HOL/Library/Binomial",
    11   "~~/src/HOL/Library/Permutation"
    12 ];
    13 
    14 
    15 (*** New development, based on explicit structures ***)
    16 
    17 use_thys [
    18   (* Groups *)
    19   "FiniteProduct",      (* Product operator for commutative groups *)
    20   "Sylow",              (* Sylow's theorem *)
    21   "Bij",                (* Automorphism Groups *)
    22 
    23   (* Rings *)
    24   "Divisibility",       (* Rings *)
    25   "IntRing",            (* Ideals and residue classes *)
    26   "UnivPoly"            (* Polynomials *)
    27 ];
    28 
    29 
    30 (*** Old development, based on axiomatic type classes ***)
    31 
    32 no_document use_thys [
    33   "abstract/Abstract",  (*The ring theory*)
    34   "poly/Polynomial"     (*The full theory*)
    35 ];