author | wenzelm |
Sat, 17 Sep 2005 20:49:14 +0200 | |
changeset 17479 | 68a7acb5f22e |
parent 11093 | 62c2e0af1d30 |
child 29665 | 2b956243d123 |
permissions | -rw-r--r-- |
7998 | 1 |
(* |
2 |
Properties of abstract class field |
|
3 |
$Id$ |
|
4 |
Author: Clemens Ballarin, started 15 November 1997 |
|
5 |
*) |
|
6 |
||
17479 | 7 |
theory Field imports Factor PID begin |
7998 | 8 |
|
17479 | 9 |
instance field < "domain" |
10 |
apply intro_classes |
|
11 |
apply (rule field_one_not_zero) |
|
12 |
apply (erule field_integral) |
|
13 |
done |
|
7998 | 14 |
|
17479 | 15 |
instance field < factorial |
16 |
apply intro_classes |
|
17 |
apply (rule TrueI) |
|
18 |
apply (erule field_fact_prime) |
|
19 |
done |
|
7998 | 20 |
|
21 |
end |