496 * New ML antiquotation @{code}: takes constant as argument, generates |
496 * New ML antiquotation @{code}: takes constant as argument, generates |
497 corresponding code in background and inserts name of the corresponding |
497 corresponding code in background and inserts name of the corresponding |
498 resulting ML value/function/datatype constructor binding in place. |
498 resulting ML value/function/datatype constructor binding in place. |
499 All occurrences of @{code} with a single ML block are generated |
499 All occurrences of @{code} with a single ML block are generated |
500 simultaneously. Provides a generic and safe interface for |
500 simultaneously. Provides a generic and safe interface for |
501 instrumentalizing code generation. See HOL/ex/Code_Antiq for a toy |
501 instrumentalizing code generation. See HOL/Decision_Procs/Ferrack for |
502 example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious |
502 a more ambitious application. In future you ought refrain from ad-hoc |
503 application. In future you ought refrain from ad-hoc compiling |
503 compiling generated SML code on the ML toplevel. Note that (for technical |
504 generated SML code on the ML toplevel. Note that (for technical |
|
505 reasons) @{code} cannot refer to constants for which user-defined |
504 reasons) @{code} cannot refer to constants for which user-defined |
506 serializations are set. Refer to the corresponding ML counterpart |
505 serializations are set. Refer to the corresponding ML counterpart |
507 directly in that cases. |
506 directly in that cases. |
508 |
507 |
509 * Integrated image HOL-Complex with HOL. Entry points Main.thy and |
508 * Integrated image HOL-Complex with HOL. Entry points Main.thy and |