| changeset 35029 | 22aab1c5e5a8 |
| parent 35027 | ed7d12bcf8f8 |
| child 35030 | f2f1e50bf65d |
--- a/NEWS Fri Feb 05 14:33:50 2010 +0100 +++ b/NEWS Mon Feb 08 10:36:02 2010 +0100 @@ -60,6 +60,9 @@ INCOMPATIBILITY. +* Index syntax for structures must be imported explicitly from library +theory Structure_Syntax. INCOMPATIBILITY. + * new theory Algebras.thy contains generic algebraic structures and generic algebraic operations. INCOMPATIBILTY: constants zero, one, plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less