author | ballarin |
Thu, 03 Aug 2006 14:57:26 +0200 | |
changeset 20318 | 0e0ea63fe768 |
parent 17479 | 68a7acb5f22e |
child 29665 | 2b956243d123 |
permissions | -rw-r--r-- |
7998 | 1 |
(* |
2 |
Principle ideal domains |
|
3 |
$Id$ |
|
4 |
Author: Clemens Ballarin, started 5 October 1999 |
|
5 |
*) |
|
6 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
17479
diff
changeset
|
7 |
theory PID imports Ideal2 begin |
7998 | 8 |
|
17479 | 9 |
instance pid < factorial |
10 |
apply intro_classes |
|
11 |
apply (rule TrueI) |
|
12 |
apply (erule pid_irred_imp_prime) |
|
13 |
done |
|
7998 | 14 |
|
15 |
end |