changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)
(* Author: Clemens Ballarin, started 5 October 1999
Principle ideal domains.
*)
theory PID
imports Ideal2
begin
instance pid < factorial
apply intro_classes
apply (erule pid_irred_imp_prime)
done
end