--- 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, \<open>\<dots>\<close>) 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}
+
\<close>