src/HOL/Algebra/ROOT.ML
author ballarin
Wed Jul 30 19:03:33 2008 +0200 (2008-07-30)
changeset 27713 95b36bfe7fc4
parent 24153 1a4607b7ad24
child 32480 6c19da8e661a
permissions -rw-r--r--
New locales for orders and lattices where the equivalence relation is not restricted to equality.
paulson@7998
     1
(*
ballarin@13936
     2
    The Isabelle Algebraic Library
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 24 September 1999
paulson@7998
     5
*)
paulson@7998
     6
ballarin@13949
     7
(* Preliminaries from set and number theory *)
ballarin@27713
     8
no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"];
wenzelm@21256
     9
ballarin@13949
    10
wenzelm@24153
    11
(*** New development, based on explicit structures ***)
ballarin@13949
    12
wenzelm@24153
    13
use_thys [
wenzelm@24153
    14
  (* Groups *)
wenzelm@24153
    15
  "FiniteProduct",      (* Product operator for commutative groups *)
wenzelm@24153
    16
  "Sylow",              (* Sylow's theorem *)
wenzelm@24153
    17
  "Bij",                (* Automorphism Groups *)
ballarin@13949
    18
wenzelm@24153
    19
  (* Rings *)
ballarin@27713
    20
  "Divisibility",       (* Rings *)
ballarin@27713
    21
  "IntRing",            (* Ideals and residue classes *)
ballarin@27713
    22
  "UnivPoly"            (* Polynomials *)
wenzelm@24153
    23
];
ballarin@20318
    24
ballarin@13936
    25
ballarin@13949
    26
(*** Old development, based on axiomatic type classes.
ballarin@13949
    27
     Will be withdrawn in future. ***)
ballarin@13936
    28
wenzelm@24153
    29
no_document use_thys [
wenzelm@24153
    30
  "abstract/Abstract",  (*The ring theory*)
wenzelm@24153
    31
  "poly/Polynomial"     (*The full theory*)
wenzelm@24153
    32
];