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

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.