author | haftmann |

Wed Feb 10 14:12:30 2010 +0100 (2010-02-10) | |

changeset 35093 | 5acba118b02a |

parent 35092 | cfe605c54e50 |

child 35094 | a0e89e47b083 |

NEWS

1.1 --- a/NEWS Wed Feb 10 14:12:04 2010 +0100 1.2 +++ b/NEWS Wed Feb 10 14:12:30 2010 +0100 1.3 @@ -22,6 +22,8 @@ 1.4 1.5 * Some generic constants have been put to appropriate theories: 1.6 1.7 + less_eq, less: Orderings 1.8 + abs, sgn: Groups 1.9 inverse, divide: Rings 1.10 1.11 INCOMPATIBILITY. 1.12 @@ -80,13 +82,9 @@ 1.13 1.14 INCOMPATIBILITY. 1.15 1.16 -* Index syntax for structures must be imported explicitly from library 1.17 -theory Structure_Syntax. INCOMPATIBILITY. 1.18 - 1.19 * New theory Algebras contains generic algebraic structures and 1.20 generic algebraic operations. INCOMPATIBILTY: constants zero, one, 1.21 -plus, minus, uminus, times, abs, sgn, less_eq and 1.22 -less have been moved from HOL.thy to Algebras.thy. 1.23 +plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy. 1.24 1.25 * HOLogic.strip_psplit: types are returned in syntactic order, similar 1.26 to other strip and tuple operations. INCOMPATIBILITY.