equal
deleted
inserted
replaced
17 interface instead. |
17 interface instead. |
18 |
18 |
19 |
19 |
20 *** Pure *** |
20 *** Pure *** |
21 |
21 |
|
22 * dropped "locale (open)". INCOMPATBILITY. |
|
23 |
22 * Command 'instance': attached definitions no longer accepted. |
24 * Command 'instance': attached definitions no longer accepted. |
23 INCOMPATIBILITY, use proper 'instantiation' target. |
25 INCOMPATIBILITY, use proper 'instantiation' target. |
24 |
26 |
25 * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
27 * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
26 |
28 |
31 demanding keyword 'by' and supporting the full method expression |
33 demanding keyword 'by' and supporting the full method expression |
32 syntax just like the Isar command 'by'. |
34 syntax just like the Isar command 'by'. |
33 |
35 |
34 |
36 |
35 *** HOL *** |
37 *** HOL *** |
|
38 |
|
39 * HOL/Orderings: added class "preorder" as superclass of "order". INCOMPATIBILITY: |
|
40 Instantiation proofs for order, linorder etc. slightly changed. Some theorems |
|
41 named order_class.* now named preorder_class.*. |
36 |
42 |
37 * HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved |
43 * HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved |
38 to separate class dvd in Ring_and_Field; a couple of lemmas on dvd has been |
44 to separate class dvd in Ring_and_Field; a couple of lemmas on dvd has been |
39 generalized to class comm_semiring_1. Likewise a bunch of lemmas from Divides |
45 generalized to class comm_semiring_1. Likewise a bunch of lemmas from Divides |
40 has been generalized from nat to class semiring_div. INCOMPATIBILITY. |
46 has been generalized from nat to class semiring_div. INCOMPATIBILITY. |