isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:2927f205abba
+:a63ca3a9b44a
 text {*
 The combinator @{ML [index] ||>>} plays a central rôle whenever your task is to update a
 theory and the update also produces a side-result (for example a theorem). Functions
 for such tasks return a pair whose second component is the theory and the fist
 component is the side-result. Using @{ML [index] ||>>}, you can do conveniently the update
-and also accumulate the side-results. Considder the following simple function.
+and also accumulate the side-results. Consider the following simple function.
 *}
 ML %linenosgray{*fun acc_incs x =
 x |> (fn x => ("", x))
 ||>> (fn x => (x, x + 1))
 ||>> (fn x => (x, x + 1))*}
 text {*
 The purpose of Line 2 is to just pair up the argument with a dummy value (since
 @{ML [index] "||>>"} operates on pairs). Each of the next three lines just increment
-the value by one, but also nest the intrermediate results to the left. For example
+the value by one, but also nest the intermediate results to the left. For example
 @{ML_response [display,gray]
 "acc_incs 1"
 "((((\"\", 1), 2), 3), 4)"}
 attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
 "maintaining a list of my_thms - rough test only!"
 text {*
-The parser @{ML [index] add_del in Attrib} is a pre-defined parser for
+The parser @{ML [index] add_del in Attrib} is a predefined parser for
 adding and deleting lemmas. Now if you prove the next lemma
 and attach to it the attribute @{text "[my_thms]"}
 *}
 lemma trueI_2[my_thms]: "True" by simp
 ML{*val my_thm_add = MyThmsData.map o Thm.add_thm
 val my_thm_del = MyThmsData.map o Thm.del_thm*}
 text {*
 where @{ML MyThmsData.map} updates the data appropriately. The
-corresponding theorem addtributes are
+corresponding theorem attributes are
 *}
 ML{*val my_add = Thm.declaration_attribute my_thm_add
 val my_del = Thm.declaration_attribute my_thm_del *}
 section {* Pretty-Printing\label{sec:pretty} *}
 text {*
 So far we printed out only plain strings without any formatting except for
-occasional explicit linebreaks using @{text [quotes] "\\n"}. This is
+occasional explicit line breaks using @{text [quotes] "\\n"}. This is
 sufficient for ``quick-and-dirty'' printouts. For something more
 sophisticated, Isabelle includes an infrastructure for properly formatting text.
 This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
 its functions do not operate on @{ML_type string}s, but on instances of the
 type:
 ML{*fun pprint prt = writeln (Pretty.string_of prt)*}
 text {*
 The point of the pretty-printing infrastructure is to give hints about how to
 layout text and let Isabelle do the actual layout. Let us first explain
-how you can insert places where a linebreak can occur. For this assume the
+how you can insert places where a line break can occur. For this assume the
 following function that replicates a string n times:
 *}
 ML{*fun rep n str = implode (replicate n str) *}
 *}
 ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
 text {*
-We deliberately chosed a large string so that is spans over more than one line.
+We deliberately chose a large string so that is spans over more than one line.
 If we print out the string using the usual ``quick-and-dirty'' method, then
 we obtain the ugly output:
 @{ML_response_fake [display,gray]
 "writeln test_str"
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 oooooooooooooobaaaaaaaaaaaar"}
 However by using pretty types you have the ability to indicate a possible
-linebreak for example at each space. You can achieve this with the function
+line break for example at each space. You can achieve this with the function
 @{ML [index] breaks in Pretty}, which expects a list of pretty types and inserts a
-possible linebreak in between every two elements in this list. To print
+possible line break in between every two elements in this list. To print
 this list of pretty types as a single string, we concatenate them
 with the function @{ML [index] blk in Pretty} as follows:
 @{ML_response_fake [display,gray]
 As can be seen, this function prints out the ``set'' so that starting
 from the second, each new line as an indentation of 2.
 If you print out something that goes beyond the capabilities of the
-standard functions, you can do realatively easily the formating
+standard functions, you can do relatively easily the formatting
 yourself. Assume you want to print out a list of items where like in ``English''
 the last two items are separated by @{text [quotes] "and"}. For this you can
 write the function
 *}
 text {*
 where Line 7 prints the beginning of the list and Line
 8 the last item. We have to use @{ML "Pretty.brk 1"} in order
 to insert a space (of length 1) before the
-@{text [quotes] "and"}. This space is also a pleace where a linebreak
+@{text [quotes] "and"}. This space is also a place where a line break
-can occur. We do the same ater the @{text [quotes] "and"}. This gives you
+can occur. We do the same after the @{text [quotes] "and"}. This gives you
 for example
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map (Pretty.str o string_of_int) (1 upto 22)
 where a space is. In Lines 4 and 5 we pretty-print the term and its type
 using the functions @{ML [index] pretty_term in Syntax} and @{ML [index]
 pretty_typ in Syntax}. We also use the function @{ML [index] quote in
 Pretty} in order to enclose the term and type inside quotation marks. In
 Line 9 we add a period right after the type without the possibility of a
-linebreak, because we do not want that a linebreak occurs there.
+line break, because we do not want that a line break occurs there.
 Now you can write
 @{ML_response_fake [display,gray]
 "tell_type @{context} @{term \"min (Suc 0)\"}"
 "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
-To see the proper linebreaking, you can try out the function on a bigger term
+To see the proper line breaking, you can try out the function on a bigger term
 and type. For example:
 @{ML_response_fake [display,gray]
 "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
 "The term \"op = (op = (op = (op = (op = op =))))\" has type

changeset 280	a63ca3a9b44a
parent 279	2927f205abba
child 281	32b4d3704415