update of comments in Isabelle file; making clear that sledgehammer can automate all theorems and lemmata right away