diff -r f7c97e64cc2a -r be23597e81db ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Thu May 16 19:56:12 2019 +0200 +++ b/ProgTutorial/Intro.thy Fri May 17 07:29:51 2019 +0200 @@ -208,12 +208,25 @@ alongside with examples. You can also install ``probes'' inside the copied code without having to recompile the whole Isabelle distribution. Such probes might be messages or printouts of variables (see chapter - \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems - probing the code with explicit print statements is the most effective method + \ref{chp:firststeps}). Moreover, PolyML contains a debugger that is also supported from Isabelle/jEdit + with breakpoints and stack inspection. + Still it seems that + probing the code with explicit print statements is an effective method for understanding what some piece of code is doing. However do not expect quick results with this! It is painful. Depending on the size of the code you are looking at, you will spend the better part of a quiet afternoon with it. And there seems to be no better way for understanding code in Isabelle. + Summarizing: + \begin{itemize} + \item Get familiar with the concepts and the applications by studying the Isabelle/Isar + reference manual and the rich set of theories and libraries in the standard distribution and the AFP. + \item Get familiar with the implementation and the best practices (like coding style, + canonical argument ordering, \\\) by reading the Isabelle/Isar implementation manual and by + browsing, reading and digesting both the code implementing a function as well and the + applications of that function. + \item Interactively experiment with the code. + \end{itemize} + \