src/HOL/Algebra/ROOT.ML

more fundamental pred-to-set conversions for range and domain by means of inductive_set

(*  Author: Clemens Ballarin, started 24 September 1999

The Isabelle Algebraic Library.
*)

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

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