equal
deleted
inserted
replaced
44 * Curried take and drop in library.ML; negative length is interpreted |
44 * Curried take and drop in library.ML; negative length is interpreted |
45 as infinity (as in chop). INCOMPATIBILITY. |
45 as infinity (as in chop). INCOMPATIBILITY. |
46 |
46 |
47 * Subgoal.FOCUS (and variants): resulting goal state is normalized as |
47 * Subgoal.FOCUS (and variants): resulting goal state is normalized as |
48 usual for resolution. Rare INCOMPATIBILITY. |
48 usual for resolution. Rare INCOMPATIBILITY. |
|
49 |
|
50 * Discontinued old TheoryDataFun with its copy/init operation -- data |
|
51 needs to be pure. Functor Theory_Data_PP retains the traditional |
|
52 Pretty.pp argument to merge, which is absent in the standard |
|
53 Theory_Data version. |
49 |
54 |
50 |
55 |
51 *** System *** |
56 *** System *** |
52 |
57 |
53 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |
58 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |