diff -r b83c75d051b7 -r a0b280dd4bc7 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Mon Jul 19 15:44:13 2010 +0100 +++ b/ProgTutorial/Intro.thy Tue Jul 20 13:34:44 2010 +0100 @@ -25,11 +25,11 @@ \medskip If your next project requires you to program on the ML-level of Isabelle, then this tutorial is for you. It will guide you through the first steps of - Isabelle programming, and also explain tricks of the trade. We also hope - the tutorial will encourage researchers to play with Isabelle and implement - new ideas. The source code of Isabelle can look intimidating, but beginners - can get by with knowledge of only a small number functions and a few basic - coding conventions. + Isabelle programming, and also explain ``tricks of the trade''. We also hope + the tutorial will encourage students and researchers to play with Isabelle + and implement new ideas. The source code of Isabelle can look intimidating, + but beginners can get by with knowledge of only a small number functions and + a few basic coding conventions. The best way to get to know the ML-level of Isabelle is by experimenting @@ -39,7 +39,7 @@ please let us know. It is impossible for us to know every environment, operating system or editor in which Isabelle is used. If you have comments, criticism or like to add to the tutorial, please feel free---you are most - welcome! The tutorial is meant to be gentle and comprehensive. To achieve + welcome!! The tutorial is meant to be gentle and comprehensive. To achieve this we need your help and feedback. *} @@ -85,7 +85,7 @@ learn from it. This tutorial contains frequently pointers to the Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is often your best friend while programming with Isabelle.\footnote{Or - hypersearch if you program using jEdit under MacOSX.} To understand the sources, + hypersearch if you work with jEdit under MacOSX.} To understand the sources, it is often also necessary to track the change history of a file or files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} for Isabelle provides convenient interfaces to query the history of @@ -109,7 +109,7 @@ These boxes correspond to how code can be processed inside the interactive environment of Isabelle. It is therefore easy to experiment with the code - that is given in this tutorial. However, for better readability we will drop + that is shown in this tutorial. However, for better readability we will drop the enclosing \isacommand{ML}~@{text "\ \ \"} and just write: @@ -135,9 +135,9 @@ Further information or pointers to files. \end{readmore} - The pointers to Isabelle files are hyperlinked to the tip of the Mercurial + Note that pointers to Isabelle files are hyperlinked to the tip of the Mercurial repository at \href{http://isabelle.in.tum.de/repos/isabelle/} - {http://isabelle.in.tum.de/repos/isabelle/}, not the latest release + {http://isabelle.in.tum.de/repos/isabelle/}, not the latest stable release of Isabelle. A few exercises are scattered around the text. Their solutions are given @@ -145,25 +145,25 @@ to solve the exercises on your own, and then look at the solutions. *} -section {* How To Understand Code in Isabelle *} +section {* How To Understand Isabelle Code *} text {* - One of the more difficult aspects of programming is to understand somebody - else's code. This is aggravated in Isabelle by the fact that many parts of - the code contain only few comments. There is one strategy that might be + One of the more difficult aspects of any kind of programming is to understand code + written by somebody else. This is aggravated in Isabelle by the fact that many parts of + the code contain none or only few comments. There is one strategy that might be helpful to navigate your way: ML is an interactive programming environment, which means you can evaluate code on the fly (for example inside an \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 + (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 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 efficient method - for understanding what some code is doing. However do not expect quick + probing the code with explicit print statements is the most effective method + for understanding what some piece of code is doing. However do not expect quick results with this! Depending on the size of the code you are looking at, - you will spend the better part of a quiet afternoon with it. But there - seems to be no better way around it. + 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. *} @@ -171,7 +171,7 @@ text {* One unpleasant aspect of any code development inside a larger system is that - one has to aim at a ``moving target''. Isabelle is no exception. Every + one has to aim at a ``moving target''. Isabelle is no exception of this. Every update lets potentially all hell break loose, because other developers have changed code you are relying on. Cursing is somewhat helpful in such situations, but taking the view that incompatible code changes are a fact of life