equal
deleted
inserted
replaced
287 |
287 |
288 * Discontinued old TheoryDataFun with its copy/init operation -- data |
288 * Discontinued old TheoryDataFun with its copy/init operation -- data |
289 needs to be pure. Functor Theory_Data_PP retains the traditional |
289 needs to be pure. Functor Theory_Data_PP retains the traditional |
290 Pretty.pp argument to merge, which is absent in the standard |
290 Pretty.pp argument to merge, which is absent in the standard |
291 Theory_Data version. |
291 Theory_Data version. |
|
292 |
|
293 * Renamed varify/unvarify operations to varify_global/unvarify_global |
|
294 to emphasize that these only work in a global situation (which is |
|
295 quite rare). |
292 |
296 |
293 |
297 |
294 *** System *** |
298 *** System *** |
295 |
299 |
296 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |
300 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |