src/HOL/Algebra/ROOT.ML
author paulson
Thu May 01 10:29:44 2003 +0200 (2003-05-01)
changeset 13943 83d842ccd4aa
parent 13940 c67798653056
child 13949 0ce528cd6f19
permissions -rw-r--r--
moving Bij.thy from GroupTheory to Algebra
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@13936
     7
(* New development, based on explicit structures *)
ballarin@13936
     8
ballarin@13940
     9
no_document use_thy "FuncSet";
ballarin@13936
    10
use_thy "Sylow";		(* Groups *)
paulson@13943
    11
use_thy "Bij";			(* Automorphism Groups *)
ballarin@13940
    12
use_thy "UnivPoly";		(* Rings and polynomials *)
ballarin@13936
    13
ballarin@13936
    14
(* Old development, based on axiomatic type classes.
ballarin@13936
    15
   Will be withdrawn in future. *)
ballarin@13936
    16
wenzelm@9000
    17
with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
wenzelm@9000
    18
with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)