diff -r f03aad9923a0 -r bc5c48dc76d0 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Fri Oct 29 12:51:44 2010 +0200 +++ b/ProgTutorial/Intro.thy Fri Oct 29 12:57:44 2010 +0200 @@ -156,7 +156,7 @@ \isacommand{ML}~@{text "\\\"} section). So you can copy (self-contained) chunks of existing code into a separate theory file and then study it alongside with examples. You can also install ``probes'' inside the - copied code without having to recompile the whole Isabelle distributions. Such + 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