# HG changeset patch # User Christian Urban # Date 1243592148 -7200 # Node ID cb86bf5658e4cde001b7ea249e6cb528074ec6aa # Parent 3cfd9a8a6de14f5f4fd0a40e98eea196b7e95be1 some slight polishing diff -r 3cfd9a8a6de1 -r cb86bf5658e4 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Thu May 28 12:15:50 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Fri May 29 12:15:48 2009 +0200 @@ -54,20 +54,22 @@ \isacommand{ML}~@{text "\ \ \"} scaffolding whenever we show code. The lines prefixed with @{text [quotes] ">"} are not part of the code, rather they indicate what the response is when the code is evaluated. - There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf}. - The first evaluates the given code, but any effect on the ambient - theory is suppressed. The second needs to be used if ML-code is defined + There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for + including ML-code. The first evaluates the given code, but any effect on the + ambient theory is suppressed. The second needs to be used if ML-code is defined inside a proof. For example -\begin{isabelle} -\isacommand{lemma}~@{text "test:"}\isanewline -\isacommand{shows}~@{text [quotes] "True"}\isanewline -\isacommand{ML\_prf}~@{text "\"}~@{ML "writeln \"Trivial\""}~@{text "\"}\isanewline -\isacommand{oops} -\end{isabelle} + \begin{quote} + \begin{isabelle} + \isacommand{lemma}~@{text "test:"}\isanewline + \isacommand{shows}~@{text [quotes] "True"}\isanewline + \isacommand{ML\_prf}~@{text "\"}~@{ML "writeln \"Trivial!\""}~@{text "\"}\isanewline + \isacommand{oops} + \end{isabelle} + \end{quote} - Inside a proof the \isacommand{ML} will generate an error message. - However, both commands will not play any role in this tutorial. + However, both commands will not play any role in this tutorial (we, for example, + always assume the ML-code is defined outside proofs). Once a portion of code is relatively stable, you usually want to export it to a separate ML-file. Such files can then be included somewhere inside a @@ -99,7 +101,7 @@ \end{tabular} \end{quote} - Note that no parentheses are given this time. + Note that no parentheses are given this time. *} section {* Debugging and Printing\label{sec:printing} *} @@ -639,7 +641,7 @@ representation corresponding to the datatype @{ML_type "term"} defined as follows: *} -ML_val{*datatype term = +ML_val %linenosgray{*datatype term = Const of string * typ | Free of string * typ | Var of indexname * typ @@ -648,8 +650,8 @@ | $ of term * term *} text {* - Terms use the usual de Bruijn index mechanism---where - bound variables are represented by the constructor @{ML Bound}. For + As can be seen in Line 5, terms use the usual de Bruijn index mechanism + for representing bound variables. For example in @{ML_response_fake [display, gray] @@ -686,12 +688,14 @@ When constructing terms, you are usually concerned with free variables (for example you cannot construct schematic variables using the antiquotation @{text "@{term \}"}). - If you deal with theorems, you have to observe the distinction. A similar + If you deal with theorems, you have to, however, observe the distinction. A similar distinction holds for types (see below). \begin{readmore} Terms and types are described in detail in \isccite{sec:terms}. Their definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. + For constructing terms involving HOL constants, many helper functions are defined + in @{ML_file "HOL/Tools/hologic.ML"}. \end{readmore} Constructing terms via antiquotations has the advantage that only typable diff -r 3cfd9a8a6de1 -r cb86bf5658e4 ProgTutorial/Intro.thy --- 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 diff -r 3cfd9a8a6de1 -r cb86bf5658e4 progtutorial.pdf Binary file progtutorial.pdf has changed