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 |
|
51 *** System *** |
|
52 |
|
53 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |
|
54 ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions. Note that |
|
55 proof terms are enabled unconditionally in the new HOL-Proofs image. |
49 |
56 |
50 |
57 |
51 |
58 |
52 New in Isabelle2009-1 (December 2009) |
59 New in Isabelle2009-1 (December 2009) |
53 ------------------------------------- |
60 ------------------------------------- |