equal
deleted
inserted
replaced
10 the user space functionality any longer. |
10 the user space functionality any longer. |
11 |
11 |
12 |
12 |
13 *** HOL *** |
13 *** HOL *** |
14 |
14 |
15 * more consistent naming of type classes involving orderings (and lattices): |
15 * More consistent naming of type classes involving orderings (and lattices): |
16 |
16 |
17 lower_semilattice ~> semilattice_inf |
17 lower_semilattice ~> semilattice_inf |
18 upper_semilattice ~> semilattice_sup |
18 upper_semilattice ~> semilattice_sup |
19 |
19 |
20 dense_linear_order ~> dense_linorder |
20 dense_linear_order ~> dense_linorder |
30 pordered_comm_ring ~> ordered_comm_ring |
30 pordered_comm_ring ~> ordered_comm_ring |
31 pordered_comm_semiring ~> ordered_comm_semiring |
31 pordered_comm_semiring ~> ordered_comm_semiring |
32 pordered_ring ~> ordered_ring |
32 pordered_ring ~> ordered_ring |
33 pordered_ring_abs ~> ordered_ring_abs |
33 pordered_ring_abs ~> ordered_ring_abs |
34 pordered_semiring ~> ordered_semiring |
34 pordered_semiring ~> ordered_semiring |
35 |
|
36 lordered_ab_group_add ~> lattice_ab_group_add |
|
37 lordered_ab_group_add_abs ~> lattice_ab_group_add_abs |
|
38 lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add |
|
39 lordered_ab_group_add_join ~> semilattice_sup_ab_group_add |
|
40 lordered_ring ~> lattice_ring |
|
41 |
35 |
42 ordered_ab_group_add ~> linordered_ab_group_add |
36 ordered_ab_group_add ~> linordered_ab_group_add |
43 ordered_ab_semigroup_add ~> linordered_ab_semigroup_add |
37 ordered_ab_semigroup_add ~> linordered_ab_semigroup_add |
44 ordered_cancel_ab_semigroup_add ~> linordered_cancel_ab_semigroup_add |
38 ordered_cancel_ab_semigroup_add ~> linordered_cancel_ab_semigroup_add |
45 ordered_comm_semiring_strict ~> linordered_comm_semiring_strict |
39 ordered_comm_semiring_strict ~> linordered_comm_semiring_strict |
55 ordered_semidom ~> linordered_semidom |
49 ordered_semidom ~> linordered_semidom |
56 ordered_semiring ~> linordered_semiring |
50 ordered_semiring ~> linordered_semiring |
57 ordered_semiring_1 ~> linordered_semiring_1 |
51 ordered_semiring_1 ~> linordered_semiring_1 |
58 ordered_semiring_1_strict ~> linordered_semiring_1_strict |
52 ordered_semiring_1_strict ~> linordered_semiring_1_strict |
59 ordered_semiring_strict ~> linordered_semiring_strict |
53 ordered_semiring_strict ~> linordered_semiring_strict |
|
54 |
|
55 The following slightly odd type classes have been moved to |
|
56 a separate theory Library/Lattice_Algebras.thy: |
|
57 |
|
58 lordered_ab_group_add ~> lattice_ab_group_add |
|
59 lordered_ab_group_add_abs ~> lattice_ab_group_add_abs |
|
60 lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add |
|
61 lordered_ab_group_add_join ~> semilattice_sup_ab_group_add |
|
62 lordered_ring ~> lattice_ring |
60 |
63 |
61 INCOMPATIBILITY. |
64 INCOMPATIBILITY. |
62 |
65 |
63 * new theory Algebras.thy contains generic algebraic structures and |
66 * new theory Algebras.thy contains generic algebraic structures and |
64 generic algebraic operations. INCOMPATIBILTY: constants zero, one, |
67 generic algebraic operations. INCOMPATIBILTY: constants zero, one, |