equal
deleted
inserted
replaced
16 \begin{flushright} |
16 \begin{flushright} |
17 {\em |
17 {\em |
18 ``We will most likely never realize the full importance of painting the Tower,\\ |
18 ``We will most likely never realize the full importance of painting the Tower,\\ |
19 that it is the essential element in the conservation of metal works and the\\ |
19 that it is the essential element in the conservation of metal works and the\\ |
20 more meticulous the paint job, the longer the tower shall endure.''} \\[1ex] |
20 more meticulous the paint job, the longer the tower shall endure.''} \\[1ex] |
21 Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been |
21 Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been |
22 re-painted 18 times since its initial construction, an average of once every |
22 re-painted 18 times since its initial construction, an average of once every |
23 seven years. It takes more than one year for a team of 25 painters to paint the tower |
23 seven years. It takes more than one year for a team of 25 painters to paint the tower |
24 from top to bottom.} |
24 from top to bottom.} |
25 \end{flushright} |
25 \end{flushright} |
26 |
26 |
293 |
293 |
294 fun pretty_thms_no_vars ctxt thms = |
294 fun pretty_thms_no_vars ctxt thms = |
295 Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*} |
295 Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*} |
296 |
296 |
297 text {* |
297 text {* |
298 Printing functions for types are |
298 Printing functions for @{ML_type typ} are |
299 *} |
299 *} |
300 |
300 |
301 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty |
301 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty |
302 fun pretty_typs ctxt tys = |
302 fun pretty_typs ctxt tys = |
303 Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*} |
303 Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*} |
304 |
304 |
305 text {* |
305 text {* |
306 respectively ctypes |
306 respectively @{ML_type ctyp} |
307 *} |
307 *} |
308 |
308 |
309 ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty) |
309 ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty) |
310 fun pretty_ctyps ctxt ctys = |
310 fun pretty_ctyps ctxt ctys = |
311 Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*} |
311 Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*} |