equal
deleted
inserted
replaced
207 |
207 |
208 * Sledgehammer: |
208 * Sledgehammer: |
209 |
209 |
210 - Renamed option: |
210 - Renamed option: |
211 isar_shrink ~> isar_compress |
211 isar_shrink ~> isar_compress |
|
212 |
|
213 * HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment. |
|
214 |
|
215 With HOL-Spec_Check, ML developers can check specifications with the |
|
216 ML function check_property. The specifications must be of the form |
|
217 "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in |
|
218 src/HOL/Spec_Check/Examples.thy. |
212 |
219 |
213 |
220 |
214 *** HOL-Algebra *** |
221 *** HOL-Algebra *** |
215 |
222 |
216 * Discontinued theories src/HOL/Algebra/abstract and .../poly. |
223 * Discontinued theories src/HOL/Algebra/abstract and .../poly. |