equal
deleted
inserted
replaced
129 different phases of code generation. See src/HOL/ex/Code_Timing.thy for |
129 different phases of code generation. See src/HOL/ex/Code_Timing.thy for |
130 examples. |
130 examples. |
131 |
131 |
132 |
132 |
133 *** HOL *** |
133 *** HOL *** |
|
134 |
|
135 * Abstract locales semigroup, abel_semigroup, semilattice, |
|
136 semilattice_neutr, ordering, ordering_top, semilattice_order, |
|
137 semilattice_neutr_order, comm_monoid_set, semilattice_set, |
|
138 semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set |
|
139 monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset, |
|
140 comm_monoid_fun use boldified syntax uniformly that does not clash |
|
141 with corresponding global syntax. INCOMPATIBILITY. |
134 |
142 |
135 * Conventional syntax "%(). t" for unit abstractions. Slight syntactic |
143 * Conventional syntax "%(). t" for unit abstractions. Slight syntactic |
136 INCOMPATIBILITY. |
144 INCOMPATIBILITY. |
137 |
145 |
138 * Command 'code_reflect' accepts empty constructor lists for datatypes, |
146 * Command 'code_reflect' accepts empty constructor lists for datatypes, |