equal
deleted
inserted
replaced
310 * Sledgehammer: |
310 * Sledgehammer: |
311 |
311 |
312 - Renamed option: |
312 - Renamed option: |
313 isar_shrink ~> isar_compress |
313 isar_shrink ~> isar_compress |
314 |
314 |
315 * HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment. |
|
316 |
|
317 With HOL-Spec_Check, ML developers can check specifications with the |
|
318 ML function check_property. The specifications must be of the form |
|
319 "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in |
|
320 src/HOL/Spec_Check/Examples.thy. |
|
321 |
|
322 * Imperative-HOL: The MREC combinator is considered legacy and no |
315 * Imperative-HOL: The MREC combinator is considered legacy and no |
323 longer included by default. INCOMPATIBILITY, use partial_function |
316 longer included by default. INCOMPATIBILITY, use partial_function |
324 instead, or import theory Legacy_Mrec as a fallback. |
317 instead, or import theory Legacy_Mrec as a fallback. |
325 |
318 |
326 * HOL-Algebra: Discontinued theories src/HOL/Algebra/abstract and |
319 * HOL-Algebra: Discontinued theories src/HOL/Algebra/abstract and |
328 src/HOL/Library/Polynomial instead. The latter provides integration |
321 src/HOL/Library/Polynomial instead. The latter provides integration |
329 with HOL's type classes for rings. INCOMPATIBILITY. |
322 with HOL's type classes for rings. INCOMPATIBILITY. |
330 |
323 |
331 |
324 |
332 *** ML *** |
325 *** ML *** |
|
326 |
|
327 * Spec_Check is a Quickcheck tool for Isabelle/ML. The ML function |
|
328 "check_property" allows to check specifications of the form "ALL x y |
|
329 z. prop x y z". See also ~~/src/Tools/Spec_Check/ with its |
|
330 Examples.thy in particular. |
333 |
331 |
334 * More uniform naming of goal functions for skipped proofs: |
332 * More uniform naming of goal functions for skipped proofs: |
335 |
333 |
336 Skip_Proof.prove ~> Goal.prove_sorry |
334 Skip_Proof.prove ~> Goal.prove_sorry |
337 Skip_Proof.prove_global ~> Goal.prove_sorry_global |
335 Skip_Proof.prove_global ~> Goal.prove_sorry_global |