--- 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.
*}