src/HOL/Algebra/abstract/PID.thy

beautified spacing for binders with symbols syntax, analogous to HOL.thy

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

PID = Ideal +

instance
  pid < factorial	(TrueI, pid_irred_imp_prime)

end