46 |
46 |
47 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals |
47 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals |
48 no longer need to be stated as "<prems> ==> False", equivalences (i.e. |
48 no longer need to be stated as "<prems> ==> False", equivalences (i.e. |
49 "=" on type bool) are handled, variable names of the form "lit_<n>" |
49 "=" on type bool) are handled, variable names of the form "lit_<n>" |
50 are no longer reserved, significant speedup. |
50 are no longer reserved, significant speedup. |
|
51 |
|
52 |
|
53 *** ML *** |
|
54 |
|
55 * Simplifier: the simpset of a running simplification process now |
|
56 contains a proof context (cf. Simplifier.the_context), which is the |
|
57 very context that the initial simpset has been retrieved from (by |
|
58 simpset_of/local_simpset_of). Consequently, all plug-in components |
|
59 (solver, looper etc.) may depend on arbitrary proof data. |
|
60 |
|
61 * Simplifier.inherit_context inherits the proof context (plus the |
|
62 local bounds) of the current simplification process; any simproc |
|
63 etc. that calls the Simplifier recursively should do this! Removed |
|
64 former Simplifier.inherit_bounds, which is already included here -- |
|
65 INCOMPATIBILITY. |
|
66 |
|
67 * Simplifier/Classical Reasoner: more abstract interfaces |
|
68 change_simpset/claset for modifying the simpset/claset reference of a |
|
69 theory; raw versions simpset/claset_ref etc. have been discontinued -- |
|
70 INCOMPATIBILITY. |
51 |
71 |
52 |
72 |
53 |
73 |
54 New in Isabelle2005 (October 2005) |
74 New in Isabelle2005 (October 2005) |
55 ---------------------------------- |
75 ---------------------------------- |