equal
deleted
inserted
replaced
106 * HOL/Cardinals: Theories of ordinals and cardinals |
106 * HOL/Cardinals: Theories of ordinals and cardinals |
107 (supersedes the AFP entry "Ordinals_and_Cardinals"). |
107 (supersedes the AFP entry "Ordinals_and_Cardinals"). |
108 |
108 |
109 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel |
109 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel |
110 execution for code generated towards Isabelle/ML. |
110 execution for code generated towards Isabelle/ML. |
|
111 |
|
112 * Library/FinFun.thy: theory of almost everywhere constant functions |
|
113 (supersedes the AFP entry "Code Generation for Functions as Data"). |
|
114 |
|
115 * Library/Phantom.thy: generic phantom type to make a type parameter |
|
116 appear in a constant's type. This alternative to adding TYPE('a) as |
|
117 another parameter avoids unnecessary closures in generated code. |
111 |
118 |
112 * Simproc "finite_Collect" rewrites set comprehensions into pointfree |
119 * Simproc "finite_Collect" rewrites set comprehensions into pointfree |
113 expressions. |
120 expressions. |
114 |
121 |
115 * Quickcheck: |
122 * Quickcheck: |