7 New in this Isabelle version |
7 New in this Isabelle version |
8 ---------------------------- |
8 ---------------------------- |
9 |
9 |
10 *** HOL *** |
10 *** HOL *** |
11 |
11 |
12 * Theory "HOL-Library.Multiset": consolidated operation and fact names |
12 * Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to |
13 multp ~> multp_code |
13 type class preorder. |
14 multeqp ~> multeqp_code |
14 |
15 multp_cancel_add_mset ~> multp_cancel_add_mset0 |
15 * Theory "HOL-Library.Multiset": |
16 multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset |
16 - Consolidated operation and fact names. |
17 multp_code_iff ~> multp_code_iff_mult |
17 multp ~> multp_code |
18 multeqp_code_iff ~> multeqp_code_iff_reflcl_mult |
18 multeqp ~> multeqp_code |
19 Minor INCOMPATIBILITY. |
19 multp_cancel_add_mset ~> multp_cancel_add_mset0 |
20 |
20 multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset |
21 * Theory "HOL-Library.Multiset": move mult1_lessE out of preorder type |
21 multp_code_iff ~> multp_code_iff_mult |
22 class and add explicit assumption. Minor INCOMPATIBILITY. |
22 multeqp_code_iff ~> multeqp_code_iff_reflcl_mult |
|
23 Minor INCOMPATIBILITY. |
|
24 - Moved mult1_lessE out of preorder type class and add explicit |
|
25 assumption. Minor INCOMPATIBILITY. |
|
26 - Added predicate multp equivalent to set mult. Reuse name previously |
|
27 used for what is now called multp_code. Minor INCOMPATIBILITY. |
23 |
28 |
24 |
29 |
25 New in Isabelle2021-1 (December 2021) |
30 New in Isabelle2021-1 (December 2021) |
26 ------------------------------------- |
31 ------------------------------------- |
27 |
32 |