87 |
87 |
88 * 'specification' command added, allowing for definition by |
88 * 'specification' command added, allowing for definition by |
89 specification. There is also an 'ax_specification' command that |
89 specification. There is also an 'ax_specification' command that |
90 introduces the new constants axiomatically. |
90 introduces the new constants axiomatically. |
91 |
91 |
92 |
|
93 * arith(_tac) is now able to generate counterexamples for reals as well. |
92 * arith(_tac) is now able to generate counterexamples for reals as well. |
94 |
93 |
95 * SET-Protocol: formalization and verification of the SET protocol suite; |
94 * SET-Protocol: formalization and verification of the SET protocol suite; |
96 |
95 |
97 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function |
96 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function |
98 defintions, thanks to Sava Krsti\'{c} and John Matthews. |
97 defintions, thanks to Sava Krsti\'{c} and John Matthews. |
|
98 |
|
99 * Unions and Intersections: |
|
100 The x-symbol output syntax of UN and INT has been changed |
|
101 from "\<Union>x \<in> A. B" to "\<Union\<^bsub>x \<in> A\<^esub> B" |
|
102 i.e. the index formulae has become a subscript, like in normal math. |
|
103 Similarly for "\<Union>x. B", and for \<Inter> instead of \<Union>. |
|
104 The subscript version is also accepted as input syntax. |
|
105 |
99 |
106 |
100 New in Isabelle2003 (May 2003) |
107 New in Isabelle2003 (May 2003) |
101 -------------------------------- |
108 -------------------------------- |
102 |
109 |
103 *** General *** |
110 *** General *** |