369 \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\ |
369 \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\ |
370 \verb!\end{center}! |
370 \verb!\end{center}! |
371 \end{quote} |
371 \end{quote} |
372 |
372 |
373 If you are not afraid of ML, you may also define your own styles. |
373 If you are not afraid of ML, you may also define your own styles. |
374 A style is simply implemented by an ML function of type \verb!term -> term!. |
374 A style is implemented by an ML function of type |
375 Have a look at the following example (which indeed shows just the way the |
375 \verb!Proof.context -> term -> term!. |
376 \verb!lhs! style is implemented): |
376 Have a look at the following example: |
|
377 |
377 \begin{quote} |
378 \begin{quote} |
378 \verb!setup {!\verb!*!\\ |
379 \verb!setup {!\verb!*!\\ |
379 \verb!let!\\ |
380 \verb!let!\\ |
380 \verb! fun my_lhs (Const ("==", _) $ t $ _) = t!\\ |
381 \verb! fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\ |
381 \verb! | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\ |
382 \verb! | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs t!\\ |
382 \verb! | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\ |
383 \verb! | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs t!\\ |
383 \verb! | my_lhs (_ $ t $ _) = t!\\ |
384 \verb! | my_lhs ctxt (_ $ t $ _) = t!\\ |
384 \verb! | my_lhs _ = error ("Binary operator expected")!\\ |
385 \verb! | my_lhs ctxt _ = error ("Binary operator expected")!\\ |
385 \verb! in [Style.put_style "new_lhs" my_lhs]!\\ |
386 \verb! in [TermStyle.update_style "new_lhs" my_lhs]!\\ |
386 \verb!end;!\\ |
387 \verb!end;!\\ |
387 \verb!*!\verb!}!\\ |
388 \verb!*!\verb!}!\\ |
388 \end{quote} |
389 \end{quote} |
|
390 |
|
391 This example indeed shows a way the \verb!lhs! style could be implemented; |
|
392 note that the real implementation is more sophisticated. |
|
393 |
389 This code must go into your theory file, not as part of your |
394 This code must go into your theory file, not as part of your |
390 \LaTeX\ text but as a separate command in front of it. |
395 \LaTeX\ text but as a separate command in front of it. |
391 Like in this example, it is recommended to put the definition of the style |
396 Like in this example, it is recommended to put the definition of the style |
392 function into a \verb!let! expression, in order not to pollute the |
397 function into a \verb!let! expression, in order not to pollute the |
393 ML global namespace. The mapping from identifier name to the style function |
398 ML global namespace. Each style receives the current proof context |
394 is done by the \verb!Style.put_style! expression which expects the desired |
399 as first argument; this is necessary in situations where the current proof |
395 style name and the style function as arguments. After this \verb!setup!, |
400 context has an impact on the style (which is the case e.~g.~when the |
396 there will be a new style available named \verb!new_lhs! allowing |
401 style has some object-logic specific behaviour). |
|
402 |
|
403 The mapping from identifier name to the style function |
|
404 is done by the \verb!Style.update_style! expression which expects the desired |
|
405 style name and the style function as arguments. |
|
406 |
|
407 After this \verb!setup!, |
|
408 there will be a new style available named \verb!new_lhs!, thus allowing |
397 antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}! |
409 antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}! |
398 yielding \isa{rev\ {\isacharparenleft}map\ f\ xs{\isacharparenright}}. |
410 yielding \isa{rev\ {\isacharparenleft}map\ f\ xs{\isacharparenright}}. |
399 |
411 |
400 The example above may be used as as a ``copy-and-paste'' pattern to write |
412 The example above may be used as as a ``copy-and-paste'' pattern to write |
401 your own styles; for a description of the constructs used, please refer |
413 your own styles; for a description of the constructs used, please refer |