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