equal
deleted
inserted
replaced
217 demanding keyword 'by' and supporting the full method expression |
217 demanding keyword 'by' and supporting the full method expression |
218 syntax just like the Isar command 'by'. |
218 syntax just like the Isar command 'by'. |
219 |
219 |
220 |
220 |
221 *** HOL *** |
221 *** HOL *** |
|
222 |
|
223 * Some set operations are now proper qualified constants with authentic syntax. |
|
224 INCOMPATIBILITY: |
|
225 |
|
226 op Int ~> Set.Int |
|
227 op Un ~> Set.Un |
|
228 INTER ~> Set.INTER |
|
229 UNION ~> Set.UNION |
|
230 Inter ~> Set.Inter |
|
231 Union ~> Set.Union |
|
232 {} ~> Set.empty |
|
233 UNIV ~> Set.UNIV |
|
234 |
|
235 * Class complete_lattice with operations Inf, Sup, INFI, SUPR now in theory |
|
236 Set. |
222 |
237 |
223 * Auxiliary class "itself" has disappeared -- classes without any parameter |
238 * Auxiliary class "itself" has disappeared -- classes without any parameter |
224 are treated as expected by the 'class' command. |
239 are treated as expected by the 'class' command. |
225 |
240 |
226 * Leibnitz's Series for Pi and the arcus tangens and logarithm series. |
241 * Leibnitz's Series for Pi and the arcus tangens and logarithm series. |
295 * If methods "eval" and "evaluation" encounter a structured proof state |
310 * If methods "eval" and "evaluation" encounter a structured proof state |
296 with !!/==>, only the conclusion is evaluated to True (if possible), |
311 with !!/==>, only the conclusion is evaluated to True (if possible), |
297 avoiding strange error messages. |
312 avoiding strange error messages. |
298 |
313 |
299 * Simplifier: simproc for let expressions now unfolds if bound variable |
314 * Simplifier: simproc for let expressions now unfolds if bound variable |
300 occurs at most one time in let expression body. INCOMPATIBILITY. |
315 occurs at most once in let expression body. INCOMPATIBILITY. |
301 |
316 |
302 * New classes "top" and "bot" with corresponding operations "top" and "bot" |
317 * New classes "top" and "bot" with corresponding operations "top" and "bot" |
303 in theory Orderings; instantiation of class "complete_lattice" requires |
318 in theory Orderings; instantiation of class "complete_lattice" requires |
304 instantiation of classes "top" and "bot". INCOMPATIBILITY. |
319 instantiation of classes "top" and "bot". INCOMPATIBILITY. |
305 |
320 |