New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series

instance for polynomial rings with characteristic zero

recovered document from 0f3fdf689bf9;

tuned;

clarified parent session images, to avoid duplicate loading of theories; avoid name conflict with loaded theory src/HOL/Library/Parallel.thy;

clarified parent session images, to avoid duplicate loading of theories;

clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;

clarified modules;

actually use theory;

clarified parent session images, to avoid duplicate loading of theories;

merged

tuned documentation;

support for potential session imports;

more checks;

tuned messages;