4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** Pure *** |
7 *** Pure *** |
8 |
8 |
9 * Code generator: details of internal data cache have no impact on |
9 * Code generator: details of internal data cache have no impact on the |
10 the user space functionality any longer. |
10 user space functionality any longer. |
11 |
11 |
12 |
12 |
13 *** HOL *** |
13 *** HOL *** |
14 |
14 |
15 * new theory Algebras.thy contains generic algebraic structures and |
15 * New theory Algebras contains generic algebraic structures and |
16 generic algebraic operations. INCOMPATIBILTY: constants zero, one, |
16 generic algebraic operations. INCOMPATIBILTY: constants zero, one, |
17 plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less |
17 plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and |
18 have been moved from HOL.thy to Algebras.thy. |
18 less have been moved from HOL.thy to Algebras.thy. |
19 |
19 |
20 * HOLogic.strip_psplit: types are returned in syntactic order, similar |
20 * HOLogic.strip_psplit: types are returned in syntactic order, similar |
21 to other strip and tuple operations. INCOMPATIBILITY. |
21 to other strip and tuple operations. INCOMPATIBILITY. |
22 |
22 |
23 * Various old-style primrec specifications in the HOL theories have been |
23 * Various old-style primrec specifications in the HOL theories have been |
24 replaced by new-style primrec, especially in theory List. The corresponding |
24 replaced by new-style primrec, especially in theory List. The corresponding |
25 constants now have authentic syntax. INCOMPATIBILITY. |
25 constants now have authentic syntax. INCOMPATIBILITY. |
26 |
26 |
27 * Reorganized theory Multiset.thy: less duplication, less historical |
27 * Reorganized theory Multiset: less duplication, less historical |
28 organization of sections, conversion from associations lists to |
28 organization of sections, conversion from associations lists to |
29 multisets, rudimentary code generation. Use insert_DiffM2 [symmetric] |
29 multisets, rudimentary code generation. Use insert_DiffM2 [symmetric] |
30 instead of elem_imp_eq_diff_union, if needed. INCOMPATIBILITY. |
30 instead of elem_imp_eq_diff_union, if needed. INCOMPATIBILITY. |
31 |
31 |
32 * Reorganized theory Sum_Type.thy; Inl and Inr now have |
32 * Reorganized theory Sum_Type; Inl and Inr now have authentic syntax. |
33 authentic syntax. INCOMPATIBILITY. |
33 INCOMPATIBILITY. |
34 |
34 |
35 * Code generation: ML and OCaml code is decorated with signatures. |
35 * Code generation: ML and OCaml code is decorated with signatures. |
36 |
36 |
37 * Complete_Lattice.thy: lemmas top_def and bot_def have been replaced |
37 * Theory Complete_Lattice: lemmas top_def and bot_def have been |
38 by the more convenient lemmas Inf_empty and Sup_empty. Dropped lemmas |
38 replaced by the more convenient lemmas Inf_empty and Sup_empty. |
39 Inf_insert_simp and Sup_insert_simp, which are subsumed by Inf_insert |
39 Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed |
40 and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ |
40 by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace |
41 and Sup_Univ. Lemmas inf_top_right and sup_bot_right subsume inf_top |
41 former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right |
42 and sup_bot respectively. INCOMPATIBILITY. |
42 subsume inf_top and sup_bot respectively. INCOMPATIBILITY. |
43 |
43 |
44 * Finite_Set.thy and List.thy: some lemmas have been generalized from |
44 * Theory Finite_Set and List: some lemmas have been generalized from |
45 sets to lattices: |
45 sets to lattices: |
46 |
46 |
47 fun_left_comm_idem_inter ~> fun_left_comm_idem_inf |
47 fun_left_comm_idem_inter ~> fun_left_comm_idem_inf |
48 fun_left_comm_idem_union ~> fun_left_comm_idem_sup |
48 fun_left_comm_idem_union ~> fun_left_comm_idem_sup |
49 inter_Inter_fold_inter ~> inf_Inf_fold_inf |
49 inter_Inter_fold_inter ~> inf_Inf_fold_inf |