74 |
74 |
75 *** HOL *** |
75 *** HOL *** |
76 |
76 |
77 * Code generation: command 'export_code' without file keyword exports |
77 * Code generation: command 'export_code' without file keyword exports |
78 code as regular theory export, which can be materialized using the |
78 code as regular theory export, which can be materialized using the |
79 command-line tool "isabelle export", or browsed in Isabelle/jEdit via |
79 command-line tool "isabelle export" or 'export_files' in the session |
80 the "isabelle-export:" file-system. To get generated code dumped into |
80 ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:" |
81 output, use "file \<open>\<close>". Minor INCOMPATIBILITY. |
81 file-system. To get generated code dumped into output, use "file \<open>\<close>". |
|
82 Minor INCOMPATIBILITY. |
82 |
83 |
83 * Simplified syntax setup for big operators under image. In rare |
84 * Simplified syntax setup for big operators under image. In rare |
84 situations, type conversions are not inserted implicitly any longer |
85 situations, type conversions are not inserted implicitly any longer |
85 and need to be given explicitly. Auxiliary abbreviations INFIMUM, |
86 and need to be given explicitly. Auxiliary abbreviations INFIMUM, |
86 SUPREMUM, UNION, INTER should now rarely occur in output and are just |
87 SUPREMUM, UNION, INTER should now rarely occur in output and are just |