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

src/HOL/Algebra/ROOT.ML

author | ballarin |

Fri May 14 19:29:22 2004 +0200 (2004-05-14) | |

changeset 14751 | 0d7850e27fed |

parent 14551 | 2cb6ff394bfb |

child 20318 | 0e0ea63fe768 |

permissions | -rw-r--r-- |

Change of theory hierarchy: Group is now based in Lattice.

1 (*

2 The Isabelle Algebraic Library

3 $Id$

4 Author: Clemens Ballarin, started 24 September 1999

5 *)

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

9 (* Preliminaries from set and number theory *)

11 no_document use_thy "FuncSet";

12 no_document use_thy "Primes";

14 (* Groups *)

16 use_thy "FiniteProduct"; (* Product operator for commutative groups *)

17 use_thy "Sylow"; (* Sylow's theorem *)

18 use_thy "Bij"; (* Automorphism Groups *)

20 (* Rings *)

22 use_thy "UnivPoly"; (* Rings and polynomials *)

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

25 Will be withdrawn in future. ***)

27 with_path "abstract" (no_document time_use_thy) "Abstract"; (*The ring theory*)

28 with_path "poly" (no_document time_use_thy) "Polynomial"; (*The full theory*)