diff -r a0b280dd4bc7 -r 520127b708e6 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Tue Jul 20 13:34:44 2010 +0100 +++ b/ProgTutorial/Intro.thy Wed Jul 28 19:09:49 2010 +0200 @@ -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 work with jEdit under MacOSX.} To understand the sources, + hypersearch if you work with jEdit.} 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 @@ -126,7 +126,7 @@ \isacommand{foobar} and so on). We use @{text "$ \"} to indicate that a command needs to be run in a UNIX-shell, for example: - @{text [display] "$ grep -R ThyOutput *"} + @{text [display] "$ grep -R Thy_Output *"} Pointers to further information and Isabelle files are typeset in \textit{italic} and highlighted as follows: