incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
(* 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