We were a group of mostly undergrads. Computer Science students.
What we did was meet once a week to discuss the reading and the exercises, or work through the exercises together. During the week we'd read the next few sections and try the exercises. Especially at first it was really slow and took a lot of effort as we weren't very comfortable with that form of logic (most of us had only previously taken an undergrad intro to discrete math class).
I personally like Isabelle very much, and if I were to start this with a new group of people I'd do it in Isabelle. Its Prover IDE in the form of Isabelle/jEdit is much nicer than Proof General or CoqIDE. I also think its presentation is a bit more immediately understandable for someone familiar with classical logic but not necessarily type theory. Isabelle/HOL is very natural from that perspective, imo.
I agree that Isabelle's jEdit integration is nice. But what would be a polished and up-to-date introduction? I think
"Concrete Semantics" is a bit heavy going for a complete beginner. No detailed explanation of proof rules, tactics etc.
It assumes some knowledge of basic functional programming, but builds up proving-related jargon quite quickly through examples with some interspersed explanations.
It doesn't discuss structured proofs with Isar, and instead focuses on the tactical style, but I think this is an advantage - it's simpler that way, and structured proofs really only benefit human readers. They're somewhat confusing to write if you don't already have a good grasp of the entire system and what is possible.
The length of that tutorial was really intimidating to me at first, but it's quite approachable and isn't all that dense. It does take some time to work through it enough to become comfortable with the system.
Thanks. When I taught myself Isabelle/HOL a couple of years ago, there was a mismatch between the Isabelle/HOL system and its description in the old version of the tutorial you point to.
What was really hampering my grasping Isabelle/HOL was the lack of a description of the overall structure of the Isabelle/HOL system. In particular, there wasn't really a good account that explains the distinction between the rules of HOL and the meta-rules of Isabelle, and how they relate. This is hand-waved away in the tutorial. Clearly the authors don't want to burden the beginner with this material. Maybe that's the right choice ... they have a lot of experience teaching this material.
A consequence of this choice is that the whole tutorial did not (and still doesn't as far as I can gather from a quick browse) include a complete listing of the logical rules (and meta rules)! As the structure of Isabelle/HOL and its (meta-)rules are not explicitly given, it becomes hard to see how tactics work. Under what conditions does it make sense to use tactic X or tactic Y or Z? Without saying what the rules are and how tactics work on them, how do you know how to proceed when Isabelle/HOL gets stuck?
If you stick only to the examples given in the tutorials and in "Concrete Semantics" this is not so much of a problem, but as soon as you work on your own proofs, you are your own. I found this to be a major stumbling block.
I wonder if Coq is better documented in this regard. Maybe not, ITPs are just complex beasts.
What we did was meet once a week to discuss the reading and the exercises, or work through the exercises together. During the week we'd read the next few sections and try the exercises. Especially at first it was really slow and took a lot of effort as we weren't very comfortable with that form of logic (most of us had only previously taken an undergrad intro to discrete math class).
I personally like Isabelle very much, and if I were to start this with a new group of people I'd do it in Isabelle. Its Prover IDE in the form of Isabelle/jEdit is much nicer than Proof General or CoqIDE. I also think its presentation is a bit more immediately understandable for someone familiar with classical logic but not necessarily type theory. Isabelle/HOL is very natural from that perspective, imo.