author | wenzelm |
Sun, 30 Jan 2011 13:02:18 +0100 | |
changeset 41648 | 6d736d983d5c |
parent 35849 | b5522b51cb1e |
permissions | -rw-r--r-- |
(* Author: Clemens Ballarin, started 15 November 1997 Properties of abstract class field. *) theory Field imports Factor PID begin instance field < "domain" apply intro_classes apply (rule field_one_not_zero) apply (erule field_integral) done instance field < factorial apply intro_classes apply (erule field_fact_prime) done end