changeset 13870 | cf947d1ec5ff |
parent 9000 | c20d58286a51 |
child 13936 | d3671b878828 |
13869:18112403c809 | 13870:cf947d1ec5ff |
---|---|
4 Author: Clemens Ballarin, started 24 September 1999 |
4 Author: Clemens Ballarin, started 24 September 1999 |
5 *) |
5 *) |
6 |
6 |
7 with_path "abstract" time_use_thy "Abstract"; (*The ring theory*) |
7 with_path "abstract" time_use_thy "Abstract"; (*The ring theory*) |
8 with_path "poly" time_use_thy "Polynomial"; (*The full theory*) |
8 with_path "poly" time_use_thy "Polynomial"; (*The full theory*) |
9 use_thy "Sylow"; |