equal
deleted
inserted
replaced
1 |
|
2 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
3 ============================================== |
2 ============================================== |
4 |
3 |
5 New in this Isabelle version |
4 New in this Isabelle version |
6 ---------------------------- |
5 ---------------------------- |
68 simplifier. |
67 simplifier. |
69 |
68 |
70 NB: At the moment, these decision procedures do not cope with mixed |
69 NB: At the moment, these decision procedures do not cope with mixed |
71 nat/int formulae where the two parts interact, such as `m < n ==> |
70 nat/int formulae where the two parts interact, such as `m < n ==> |
72 int(m) < int(n)'. |
71 int(m) < int(n)'. |
|
72 |
|
73 * New bounded quantifier syntax (input only): |
|
74 ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P |
73 |
75 |
74 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization |
76 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization |
75 -- avoids syntactic ambiguities and treats state, transition, and |
77 -- avoids syntactic ambiguities and treats state, transition, and |
76 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
78 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
77 changed syntax and (many) tactics; |
79 changed syntax and (many) tactics; |