198 * HOL/Cardinals: Theories of ordinals and cardinals |
198 * HOL/Cardinals: Theories of ordinals and cardinals |
199 (supersedes the AFP entry "Ordinals_and_Cardinals"). |
199 (supersedes the AFP entry "Ordinals_and_Cardinals"). |
200 |
200 |
201 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel |
201 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel |
202 execution for code generated towards Isabelle/ML. |
202 execution for code generated towards Isabelle/ML. |
|
203 |
|
204 * Library/FuncSet.thy: Extended support for Pi and extensional and introduce the |
|
205 extensional dependent function space "PiE". Replaces extensional_funcset by an |
|
206 abbreviation, rename a couple of lemmas from extensional_funcset to PiE: |
|
207 |
|
208 extensional_empty ~> PiE_empty |
|
209 extensional_funcset_empty_domain ~> PiE_empty_domain |
|
210 extensional_funcset_empty_range ~> PiE_empty_range |
|
211 extensional_funcset_arb ~> PiE_arb |
|
212 extensional_funcset_mem > PiE_mem |
|
213 extensional_funcset_extend_domainI ~> PiE_fun_upd |
|
214 extensional_funcset_restrict_domain ~> fun_upd_in_PiE |
|
215 extensional_funcset_extend_domain_eq ~> PiE_insert_eq |
|
216 card_extensional_funcset ~> card_PiE |
|
217 finite_extensional_funcset ~> finite_PiE |
|
218 |
|
219 INCOMPATIBUILITY. |
203 |
220 |
204 * Library/FinFun.thy: theory of almost everywhere constant functions |
221 * Library/FinFun.thy: theory of almost everywhere constant functions |
205 (supersedes the AFP entry "Code Generation for Functions as Data"). |
222 (supersedes the AFP entry "Code Generation for Functions as Data"). |
206 |
223 |
207 * Library/Phantom.thy: generic phantom type to make a type parameter |
224 * Library/Phantom.thy: generic phantom type to make a type parameter |