src/HOL/Algebra/abstract/PID.thy

theorem(_i): locale atts;
added add_locale;

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

PID = Ideal +

instance
  pid < factorial	(TrueI, pid_irred_imp_prime)

end