equal
deleted
inserted
replaced
86 * Update of State and Preview panels to use new WebviewPanel API of |
86 * Update of State and Preview panels to use new WebviewPanel API of |
87 VSCode. |
87 VSCode. |
88 |
88 |
89 |
89 |
90 *** HOL *** |
90 *** HOL *** |
|
91 |
|
92 * Removed multiplicativity assumption from normalization_semidom typeclass. |
|
93 Introduced various new intermediate typeclasses with the multiplicativity |
|
94 assumption; many theorem statements (especially involving GCD/LCM) had |
|
95 to be adapted. This allows for a more natural instantiation of the |
|
96 algebraic typeclasses for e.g. Gaussian integers. INCOMPATIBILITY. |
91 |
97 |
92 * Improvements of the 'lift_bnf' command: |
98 * Improvements of the 'lift_bnf' command: |
93 - Add support for quotient types. |
99 - Add support for quotient types. |
94 - Generate transfer rules for the lifted map/set/rel/pred constants |
100 - Generate transfer rules for the lifted map/set/rel/pred constants |
95 (theorems "<type>.<constant>_transfer_raw"). |
101 (theorems "<type>.<constant>_transfer_raw"). |