equal
deleted
inserted
replaced
83 way things are actually implemented. More importantly, it is often |
83 way things are actually implemented. More importantly, it is often |
84 good to look at code that does similar things as you want to do and |
84 good to look at code that does similar things as you want to do and |
85 learn from it. This tutorial contains frequently pointers to the |
85 learn from it. This tutorial contains frequently pointers to the |
86 Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is |
86 Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is |
87 often your best friend while programming with Isabelle.\footnote{Or |
87 often your best friend while programming with Isabelle.\footnote{Or |
88 hypersearch if you work with jEdit under MacOSX.} To understand the sources, |
88 hypersearch if you work with jEdit.} To understand the sources, |
89 it is often also necessary to track the change history of a file or |
89 it is often also necessary to track the change history of a file or |
90 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
90 files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} |
91 for Isabelle provides convenient interfaces to query the history of |
91 for Isabelle provides convenient interfaces to query the history of |
92 files and ``change sets''. |
92 files and ``change sets''. |
93 \end{description} |
93 \end{description} |
124 The user-level commands of Isabelle (i.e., the non-ML code) are written |
124 The user-level commands of Isabelle (i.e., the non-ML code) are written |
125 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
125 in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply}, |
126 \isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a |
126 \isacommand{foobar} and so on). We use @{text "$ \<dots>"} to indicate that a |
127 command needs to be run in a UNIX-shell, for example: |
127 command needs to be run in a UNIX-shell, for example: |
128 |
128 |
129 @{text [display] "$ grep -R ThyOutput *"} |
129 @{text [display] "$ grep -R Thy_Output *"} |
130 |
130 |
131 Pointers to further information and Isabelle files are typeset in |
131 Pointers to further information and Isabelle files are typeset in |
132 \textit{italic} and highlighted as follows: |
132 \textit{italic} and highlighted as follows: |
133 |
133 |
134 \begin{readmore} |
134 \begin{readmore} |