equal
deleted
inserted
replaced
294 
294 
295 * Pure/General: name_mangler.ML provides a functor for generic name 
295 * Pure/General: name_mangler.ML provides a functor for generic name 
296 mangling (bijective mapping from any expression values to strings). 
296 mangling (bijective mapping from any expression values to strings). 
297 
297 
298 * Pure/General: rat.ML implements rational numbers. 
298 * Pure/General: rat.ML implements rational numbers. 

299 

300 * Pure: datatype Context.generic joins theory/Proof.context and 

301 provides some facilities for generic code that works in either kind of 

302 context, notably GenericDataFun for uniform theory and proof data. 

303 

304 * Pure: type Context.generic attribute is now the preferred 

305 representation for global vs. local attributes while avoiding code 

306 duplication; Attrib.theory/context/generic converts between different 

307 types of attributes. Various Pure/HOL/ZF packages work with generic 

308 attributes now, INCOMPATIBILITY. 
299 
309 
300 * Pure: several functions of signature "... > theory > theory * ..." 
310 * Pure: several functions of signature "... > theory > theory * ..." 
301 have been reoriented to "... > theory > ... * theory" in order to 
311 have been reoriented to "... > theory > ... * theory" in order to 
302 allow natural usage in combination with the >, >>, > and 
312 allow natural usage in combination with the >, >>, > and 
303 fold_map combinators. 
313 fold_map combinators. 