35849
|
1 |
(* Author: Clemens Ballarin, started 5 October 1999
|
|
2 |
|
|
3 |
Principle ideal domains.
|
7998
|
4 |
*)
|
|
5 |
|
35849
|
6 |
theory PID
|
|
7 |
imports Ideal2
|
|
8 |
begin
|
7998
|
9 |
|
17479
|
10 |
instance pid < factorial
|
|
11 |
apply intro_classes
|
|
12 |
apply (erule pid_irred_imp_prime)
|
|
13 |
done
|
7998
|
14 |
|
|
15 |
end
|