equal
deleted
inserted
replaced
57 |
57 |
58 * Theory List: added transpose. |
58 * Theory List: added transpose. |
59 |
59 |
60 |
60 |
61 *** ML *** |
61 *** ML *** |
|
62 |
|
63 * Renamed old-style Drule.standard to Drule.export_without_context, to |
|
64 emphasize that this is in no way a standard operation. |
|
65 INCOMPATIBILITY. |
62 |
66 |
63 * Curried take and drop in library.ML; negative length is interpreted |
67 * Curried take and drop in library.ML; negative length is interpreted |
64 as infinity (as in chop). INCOMPATIBILITY. |
68 as infinity (as in chop). INCOMPATIBILITY. |
65 |
69 |
66 * Subgoal.FOCUS (and variants): resulting goal state is normalized as |
70 * Subgoal.FOCUS (and variants): resulting goal state is normalized as |