equal
deleted
inserted
replaced
26 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied |
26 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied |
27 with some care where this is really required. |
27 with some care where this is really required. |
28 |
28 |
29 |
29 |
30 *** HOL *** |
30 *** HOL *** |
|
31 |
|
32 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel |
|
33 execution for code generated towards Isabelle/ML. |
31 |
34 |
32 * Simproc "finite_Collect" rewrites set comprehensions into pointfree |
35 * Simproc "finite_Collect" rewrites set comprehensions into pointfree |
33 expressions. |
36 expressions. |
34 |
37 |
35 * Quickcheck: |
38 * Quickcheck: |