summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.

1 (*

2 The Isabelle Algebraic Library

3 $Id$

4 Author: Clemens Ballarin, started 24 September 1999

5 *)

7 (* Preliminaries from set and number theory *)

8 no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"];

11 (*** New development, based on explicit structures ***)

13 use_thys [

14 (* Groups *)

15 "FiniteProduct", (* Product operator for commutative groups *)

16 "Sylow", (* Sylow's theorem *)

17 "Bij", (* Automorphism Groups *)

19 (* Rings *)

20 "Divisibility", (* Rings *)

21 "IntRing", (* Ideals and residue classes *)

22 "UnivPoly" (* Polynomials *)

23 ];

26 (*** Old development, based on axiomatic type classes.

27 Will be withdrawn in future. ***)

29 no_document use_thys [

30 "abstract/Abstract", (*The ring theory*)

31 "poly/Polynomial" (*The full theory*)

32 ];