Mercurial Mercurial > hg > isabelle-cookbook / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/Intro.thy
changeset 254 cb86bf5658e4
parent 252 f380b13b25a7
child 262 e0049c842785 
--- a/ProgTutorial/Intro.thy	Thu May 28 12:15:50 2009 +0200
+++ b/ProgTutorial/Intro.thy	Fri May 29 12:15:48 2009 +0200
@@ -10,7 +10,7 @@
   Isabelle programming, and also explain tricks of the trade. 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 code.\footnote{\input{version}} If something does not work, 
+  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 
@@ -60,7 +60,7 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  learn from it. The GNU/UNIX command \mbox{@{text "grep -R"}} is
+  learn from it. The UNIX command \mbox{@{text "grep -R"}} is
   often your best friend while programming with Isabelle, or
   hypersearch if you program using jEdit under MacOSX.
   \end{description}
@@ -122,8 +122,8 @@
 section {* Some Naming Conventions in the Isabelle Sources *}
 
 text {*
-  There are a few naming conventions in Isabelle that might aid reading 
-  and writing code. (Remember that code is written once, but read numerous 
+  There are a few naming conventions in the Isabelle code that might aid reading 
+  and writing code. (Remember that code is written once, but read many 
   times.) The most important conventions are:
 
   \begin{itemize}
@@ -170,7 +170,7 @@
   chapter and also contributed the material on @{text NamedThmsFun}.
 
   \item {\bf Christian Sternagel} proofread the tutorial and made 
-  comments on the text. 
+  many comments on the text. 
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining
isabelle-cookbook