ProgTutorial/Intro.thy
changeset 356 43df2d59fb98
parent 353 e73ccbed776e
child 358 9cf3bc448210
--- 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.
 *}