I'm trying to learn to use Isabelle/HOL. I thought, "Hey, a tutorial written by some of the folks who developed it would be great", and so looked at https://isabelle.in.tum.de/doc/tutorial.pdf which has a publication date of Aug 15, 2018. In trying to work through examples, though, I find things like this in the text:
"The classic Isabelle user interface is Proof General / Emacs by David Aspinall’s. This book says very little about Proof General, which has its own documentation." (page iii)
"If anything strange happens, we recommend that you ask Isabelle to display all type information via the Proof General menu item Isabelle > Settings > Show Types (see Sect. 1.5 for details)." (page 5)
The problem is that Proof General appears to no longer work with Isabelle (see Isabelle2016 and Proof General). I'm baffled on why a tutorial would base itself on out-of-date software, but my real question is this:
"Is there somewhere that I can learn to do even the simplest things in Isabelle 2017?"
As of 2018, the only IDE that is supported for Isabelle is Isabelle/jEdit, which is included in the distribution you can download from the Isabelle website. There is an experimental VSCode plugin that is under active development, but I would recommend using Isabelle/jEdit for the time being.
The tutorial you found is listed on the website as one of the ‘Old Manuals’. It is severely outdated in many respects and should not be used anymore. The publication date is probably meaningless since it is the date of when the PDF was generated, not when the text was written. Some people have lobbied to have that tutorial removed from the website entirely, and your experience seems to confirm that we should indeed do that.
One of the best ways to start learning Isabelle is probably the book ‘Concrete Semantics’ (free online version available). Its first half is basically an introduction to Isabelle/HOL with lots of exercises. There is also the ‘Programming and Proving’ tutorial on the Isabelle website, which is almost identical to the first half of ‘Concrete Semantics’.
However, it focuses on applications in computer science (semantics of programming languages and a bit of functional programming). I'm not sure if there is a good tutorial about how to do mathematics in Isabelle; in any case, mathematics tends to be more difficult to do in a theorem prover for beginners because the gap to informal paper reasoning is larger. So I recommend ‘Concrete Semantics’ even if you are ultimately interested in formalising mathematics.
By the way: You mentioned Isabelle2017, but there really is no reason to use that instead of Isabelle2018, which is the most recent version at the time of writing this answer.