src/HOL/Algebra/abstract/PID.thy

now included in Complex/README.html

(*
    Principle ideal domains
    $Id$
    Author: Clemens Ballarin, started 5 October 1999
*)

PID = Ideal +

instance
  pid < factorial	(TrueI, pid_irred_imp_prime)

end