17 interface instead. |
17 interface instead. |
18 |
18 |
19 |
19 |
20 *** Pure *** |
20 *** Pure *** |
21 |
21 |
22 * Command 'instance': attached definitions now longer accepted. |
22 * Command 'instance': attached definitions no longer accepted. |
23 INCOMPATIBILITY, use proper 'instantiation' target. |
23 INCOMPATIBILITY, use proper 'instantiation' target. |
24 |
24 |
25 * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
25 * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
|
26 |
|
27 |
|
28 *** Document preparation *** |
|
29 |
|
30 * Antiquotation @{lemma} now imitates a regular terminal proof, |
|
31 demanding keyword 'by' and supporting the full method expression |
|
32 syntax just like the Isar command 'by'. |
|
33 |
|
34 |
|
35 *** HOL *** |
|
36 |
|
37 * 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 |
|
39 generalized to class comm_semiring_1. Likewise a bunch of lemmas from Divides |
|
40 has been generalized from nat to class semiring_div. INCOMPATIBILITY. |
|
41 This involves the following theorem renames resulting from duplicate elimination: |
|
42 |
|
43 dvd_def_mod ~> dvd_eq_mod_eq_0 |
|
44 zero_dvd_iff ~> dvd_0_left_iff |
|
45 DIVISION_BY_ZERO_DIV ~> div_by_0 |
|
46 DIVISION_BY_ZERO_MOD ~> mod_by_0 |
|
47 mult_div ~> div_mult_self2_is_id |
|
48 mult_mod ~> mod_mult_self2_is_0 |
|
49 |
|
50 * HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, |
|
51 zlcm (for int); carried together from various gcd/lcm developements in |
|
52 the HOL Distribution. zgcd and zlcm replace former igcd and ilcm; |
|
53 corresponding theorems renamed accordingly. INCOMPATIBILY. To |
|
54 recover tupled syntax, use syntax declarations like: |
|
55 |
|
56 hide (open) const gcd |
|
57 abbreviation gcd where |
|
58 "gcd == (%(a, b). GCD.gcd a b)" |
|
59 notation (output) |
|
60 GCD.gcd ("gcd '(_, _')") |
|
61 |
|
62 (analogously for lcm, zgcd, zlcm). |
|
63 |
|
64 * HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
26 |
65 |
27 * New ML antiquotation @{code}: takes constant as argument, generates |
66 * New ML antiquotation @{code}: takes constant as argument, generates |
28 corresponding code in background and inserts name of the corresponding |
67 corresponding code in background and inserts name of the corresponding |
29 resulting ML value/function/datatype constructor binding in place. |
68 resulting ML value/function/datatype constructor binding in place. |
30 All occurrences of @{code} with a single ML block are generated |
69 All occurrences of @{code} with a single ML block are generated |
34 application. In future you ought refrain from ad-hoc compiling |
73 application. In future you ought refrain from ad-hoc compiling |
35 generated SML code on the ML toplevel. Note that (for technical |
74 generated SML code on the ML toplevel. Note that (for technical |
36 reasons) @{code} cannot refer to constants for which user-defined |
75 reasons) @{code} cannot refer to constants for which user-defined |
37 serializations are set. Refer to the corresponding ML counterpart |
76 serializations are set. Refer to the corresponding ML counterpart |
38 directly in that cases. |
77 directly in that cases. |
39 |
|
40 |
|
41 *** Document preparation *** |
|
42 |
|
43 * Antiquotation @{lemma} now imitates a regular terminal proof, |
|
44 demanding keyword 'by' and supporting the full method expression |
|
45 syntax just like the Isar command 'by'. |
|
46 |
|
47 |
|
48 *** HOL *** |
|
49 |
|
50 * HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, |
|
51 zlcm (for int); carried together from various gcd/lcm developements in |
|
52 the HOL Distribution. zgcd and zlcm replace former igcd and ilcm; |
|
53 corresponding theorems renamed accordingly. INCOMPATIBILY. To |
|
54 recover tupled syntax, use syntax declarations like: |
|
55 |
|
56 hide (open) const gcd |
|
57 abbreviation gcd where |
|
58 "gcd == (%(a, b). GCD.gcd a b)" |
|
59 notation (output) |
|
60 GCD.gcd ("gcd '(_, _')") |
|
61 |
|
62 (analogously for lcm, zgcd, zlcm). |
|
63 |
|
64 * HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
|
65 |
78 |
66 * Integrated image HOL-Complex with HOL. Entry points Main.thy and |
79 * Integrated image HOL-Complex with HOL. Entry points Main.thy and |
67 Complex_Main.thy remain as they are. |
80 Complex_Main.thy remain as they are. |
68 |
81 |
69 * New image HOL-Plain provides a minimal HOL with the most important |
82 * New image HOL-Plain provides a minimal HOL with the most important |