equal
deleted
inserted
replaced
114 * 'specification' command added, allowing for definition by |
114 * 'specification' command added, allowing for definition by |
115 specification. There is also an 'ax_specification' command that |
115 specification. There is also an 'ax_specification' command that |
116 introduces the new constants axiomatically. |
116 introduces the new constants axiomatically. |
117 |
117 |
118 * arith(_tac) is now able to generate counterexamples for reals as well. |
118 * arith(_tac) is now able to generate counterexamples for reals as well. |
|
119 |
|
120 * HOL-Algebra: new locale "ring" for non-commutative rings. |
119 |
121 |
120 * SET-Protocol: formalization and verification of the SET protocol suite; |
122 * SET-Protocol: formalization and verification of the SET protocol suite; |
121 |
123 |
122 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function |
124 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function |
123 defintions, thanks to Sava Krsti\'{c} and John Matthews. |
125 defintions, thanks to Sava Krsti\'{c} and John Matthews. |