equal
deleted
inserted
replaced
361 mangling (bijective mapping from any expression values to strings). |
361 mangling (bijective mapping from any expression values to strings). |
362 |
362 |
363 * Pure/General/rat.ML implements rational numbers. |
363 * Pure/General/rat.ML implements rational numbers. |
364 |
364 |
365 * Pure/General/table.ML: the join operations now works via exceptions |
365 * Pure/General/table.ML: the join operations now works via exceptions |
366 DUP/SAME instead of type option. This is simpler in simple cases, and |
366 DUP/SAME instead of type option. This is both simpler and admits |
367 admits slightly more efficient complex applications. |
367 slightly more efficient complex applications. |
368 |
368 |
369 * Pure: datatype Context.generic joins theory/Proof.context and |
369 * Pure: datatype Context.generic joins theory/Proof.context and |
370 provides some facilities for code that works in either kind of |
370 provides some facilities for code that works in either kind of |
371 context, notably GenericDataFun for uniform theory and proof data. |
371 context, notably GenericDataFun for uniform theory and proof data. |
372 |
372 |