equal
deleted
inserted
replaced
31 assumption. Minor INCOMPATIBILITY. |
31 assumption. Minor INCOMPATIBILITY. |
32 - Added predicate multp equivalent to set mult. Reuse name previously |
32 - Added predicate multp equivalent to set mult. Reuse name previously |
33 used for what is now called multp_code. Minor INCOMPATIBILITY. |
33 used for what is now called multp_code. Minor INCOMPATIBILITY. |
34 - Lifted multiple lemmas from mult to multp. |
34 - Lifted multiple lemmas from mult to multp. |
35 - Redefined less_multiset to be based on multp. INCOMPATIBILITY. |
35 - Redefined less_multiset to be based on multp. INCOMPATIBILITY. |
|
36 |
|
37 * Sledgehammer: |
|
38 - Introduced sledgehammer_outcome data type and changed return type of ML |
|
39 function Sledgehammer.run_sledgehammer from "bool * (string * string list)" |
|
40 to "bool * (sledgehammer_outcome * string)". The former value can be |
|
41 recomputed with "apsnd (ATP_Util.map_prod |
|
42 Sledgehammer.short_string_of_sledgehammer_outcome single)". |
|
43 INCOMPATIBILITY. |
|
44 - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions |
|
45 in TH0 and TH1. |
36 |
46 |
37 |
47 |
38 New in Isabelle2021-1 (December 2021) |
48 New in Isabelle2021-1 (December 2021) |
39 ------------------------------------- |
49 ------------------------------------- |
40 |
50 |