diff -r 42a1c230daff -r 43df2d59fb98 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Tue Oct 20 12:25:20 2009 +0200 +++ b/ProgTutorial/Intro.thy Thu Oct 22 02:03:14 2009 +0200 @@ -26,14 +26,20 @@ 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. The best way to - get to know the ML-level of Isabelle is by experimenting with the many code - examples included in the tutorial. The code is as far as possible checked - against the Isabelle distribution.\footnote{\input{version}} If something does not work, - then 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 + the tutorial will encourage researchers to play with Isabelle and implement + new ideas. The sources 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 + with the many code examples included in the tutorial. The code is as far as + possible checked against the Isabelle + distribution.\footnote{\input{version}} If something does not work, then + 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 this we need your feedback. *}