src/HOL/Algebra/abstract/PID.thy

replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style

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

PID = Ideal +

instance
  pid < factorial	(TrueI, pid_irred_imp_prime)

end