equal
deleted
inserted
replaced
175 ALL x<=y. P, EX x<y. P, EX x<=y. P; |
175 ALL x<=y. P, EX x<y. P, EX x<=y. P; |
176 |
176 |
177 * HOL basic syntax simplified (more orthogonal): all variants of |
177 * HOL basic syntax simplified (more orthogonal): all variants of |
178 All/Ex now support plain / symbolic / HOL notation; plain syntax for |
178 All/Ex now support plain / symbolic / HOL notation; plain syntax for |
179 Eps operator is provided as well: "SOME x. P[x]"; |
179 Eps operator is provided as well: "SOME x. P[x]"; |
|
180 |
|
181 * HOL/Sum: sum_case renamed to basic_sum_case; hardly an |
|
182 INCOMPATIBILITY, users should refer to the version of HOL/Datatype; |
180 |
183 |
181 |
184 |
182 *** LK *** |
185 *** LK *** |
183 |
186 |
184 * the notation <<...>> is now available as a notation for sequences of |
187 * the notation <<...>> is now available as a notation for sequences of |