equal
deleted
inserted
replaced
195 functors with support for mixed, nested recursion and interesting 
195 functors with support for mixed, nested recursion and interesting 
196 nonfree datatypes. 
196 nonfree datatypes. 
197 
197 
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 

201 * HOL/Probability: 

202  Add simproc "measurable" to automatically prove measurability 

203 

204  Add induction rules for sigma sets with disjoint union (sigma_sets_induct_disjoint) 

205 and for Borelmeasurable functions (borel_measurable_induct). 

206 

207  The DaniellKolmogorov theorem (the existence the limit of a projective family) 
200 
208 
201 * Library/Countable_Set.thy: Theory of countable sets. 
209 * Library/Countable_Set.thy: Theory of countable sets. 
202 
210 
203 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel 
211 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel 
204 execution for code generated towards Isabelle/ML. 
212 execution for code generated towards Isabelle/ML. 