src/HOL/Algebra/abstract/PID.thy

reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp

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

PID = Ideal +

instance
  pid < factorial	(TrueI, pid_irred_imp_prime)

end