23 Superseedes some immature attempts. |
23 Superseedes some immature attempts. |
24 |
24 |
25 |
25 |
26 *** HOL *** |
26 *** HOL *** |
27 |
27 |
|
28 * Merged theories IntDef, Numeral and IntArith into unified theory Int. |
|
29 INCOMPATIBILITY. |
|
30 |
|
31 * Theory Library/Code_Index: type "index" now represents natural numbers rather |
|
32 than integers. INCOMPATIBILITY. |
|
33 |
28 * New class "uminus" with operation "uminus" (split of from class "minus" |
34 * New class "uminus" with operation "uminus" (split of from class "minus" |
29 which now only has operation "minus", binary). |
35 which now only has operation "minus", binary). INCOMPATIBILITY. |
30 |
36 |
31 * New primrec package. Specification syntax conforms in style to |
37 * New primrec package. Specification syntax conforms in style to |
32 definition/function/.... No separate induction rule is provided. |
38 definition/function/.... No separate induction rule is provided. |
33 The "primrec" command distinguishes old-style and new-style specifications |
39 The "primrec" command distinguishes old-style and new-style specifications |
34 by syntax. The former primrec package is now named OldPrimrecPackage. |
40 by syntax. The former primrec package is now named OldPrimrecPackage. |
38 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. |
44 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. |
39 |
45 |
40 * Library/ListSpace: new theory of arithmetic vector operations. |
46 * Library/ListSpace: new theory of arithmetic vector operations. |
41 |
47 |
42 * Constants "card", "internal_split", "option_map" now with authentic |
48 * Constants "card", "internal_split", "option_map" now with authentic |
43 syntax. |
49 syntax. INCOMPATIBILITY. |
44 |
50 |
45 * Definitions subset_def, psubset_def, set_diff_def, Compl_def, |
51 * Definitions subset_def, psubset_def, set_diff_def, Compl_def, |
46 le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def, |
52 le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def, |
47 sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, |
53 sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, |
48 Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def, |
54 Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def, |
49 Sup_set_def, le_def, less_def, option_map_def now with object |
55 Sup_set_def, le_def, less_def, option_map_def now with object |
50 equality. |
56 equality. INCOMPATIBILITY. |
51 |
57 |
52 * New method "induction_scheme" derives user-specified induction rules |
58 * New method "induction_scheme" derives user-specified induction rules |
53 from wellfounded induction and completeness of patterns. This factors |
59 from wellfounded induction and completeness of patterns. This factors |
54 out some operations that are done internally by the function package |
60 out some operations that are done internally by the function package |
55 and makes them available separately. See "HOL/ex/Induction_Scheme.thy" |
61 and makes them available separately. See "HOL/ex/Induction_Scheme.thy" |