diff -r 1ca2f41770cc -r 79202e2eab6a ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Wed Aug 19 09:25:49 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Thu Aug 20 10:38:26 2009 +0200 @@ -239,13 +239,13 @@ A @{ML_type cterm} can be transformed into a string by the following function. *} -ML{*fun string_of_cterm ctxt t = - string_of_term ctxt (term_of t)*} +ML{*fun string_of_cterm ctxt ct = + string_of_term ctxt (term_of ct)*} text {* - In this example the function @{ML [index] term_of} extracts the @{ML_type term} from - a @{ML_type cterm}. More than one @{ML_type cterm}s can again be printed - with @{ML [index] commas}. + In this example the function @{ML [index] term_of} extracts the @{ML_type + term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can again be + printed with @{ML [index] commas}. *} ML{*fun string_of_cterms ctxt cts = @@ -261,16 +261,19 @@ text {* Theorems also include schematic variables, such as @{text "?P"}, - @{text "?Q"} and so on. + @{text "?Q"} and so on. They are needed in order to able to + instantiate theorems when they are applied. For example the theorem + @{thm [source] conjI} shown below can be used for any (typable) + instantiation of @{text "?P"} and @{text "?Q"} @{ML_response_fake [display, gray] "tracing (string_of_thm @{context} @{thm conjI})" "\?P; ?Q\ \ ?P \ ?Q"} - In order to improve the readability of theorems we convert these schematic - variables into free variables using the function @{ML [index] import in - Variable}. This is similar to statements like @{text "conjI[no_vars]"} - from Isabelle's user-level. + However, in order to improve the readability when printing theorems, we + convert these schematic variables into free variables using the function + @{ML [index] import in Variable}. This is similar to statements like @{text + "conjI[no_vars]"} from Isabelle's user-level. *} ML{*fun no_vars ctxt thm = @@ -300,10 +303,10 @@ commas (map (string_of_thm_no_vars ctxt) thms) *} text {* - When printing out several parcels of information that semantically - belong together, like a warning message consisting for example - of a term and a type, you should try to keep this information - together in a single string. So do not print out information as + Note, that when printing out several parcels of information that + semantically belong together, like a warning message consisting for example + of a term and a type, you should try to keep this information together in a + single string. So do not print out information as @{ML_response_fake [display,gray] "tracing \"First half,\"; @@ -520,8 +523,8 @@ ML{*fun (x, y) ||> f = (x, f y)*} text {* - These two functions can be used to avoid explicit @{text "lets"} for - intermediate values in functions that return pairs. Suppose for example you + These two functions can, for example, be used to avoid explicit @{text "lets"} for + intermediate values in functions that return pairs. As an example, suppose you want to separate a list of integers into two lists according to a treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}. This function can be @@ -549,9 +552,9 @@ else separate i xs |>> cons x*} text {* - avoiding the explicit @{text "let"}. While in this example the gain is only - small, in more complicated situations the benefit of avoiding @{text "lets"} - can be substantial. + avoiding the explicit @{text "let"}. While in this example the gain in + conciseness is only small, in more complicated situations the benefit of + avoiding @{text "lets"} can be substantial. With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair. This combinator is defined as @@ -617,7 +620,7 @@ text {* - When using combinators for writing function in waterfall fashion, it is + When using combinators for writing functions in waterfall fashion, it is sometimes necessary to do some ``plumbing'' in order to fit functions together. We have already seen such plumbing in the function @{ML apply_fresh_args}, where @{ML curry} is needed for making the function @{ML @@ -643,9 +646,9 @@ In this example we obtain two terms with appropriate typing. However, if you have only a single term, then @{ML check_terms in Syntax} needs to be adapted. This can be done with the ``plumbing'' function @{ML - singleton}.\footnote{There is in fact alread a function @{ML check_term in Syntax}, - which however is defined in terms of @{ML singleton} and @{ML check_terms in - Syntax}.} For example + singleton}.\footnote{There is already a function @{ML check_term in Syntax} + in the Isabelle sources that is defined in terms of @{ML singleton} and @{ML + check_terms in Syntax}.} For example @{ML_response_fake [display, gray] "let