summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 29 Sep 1997 15:39:28 +0200 | |

changeset 3744 | 9921561ade57 |

parent 3743 | fec0f996ae67 |

child 3745 | 4c5d3b1ddc75 |

tuned;

--- a/NEWS Mon Sep 29 15:16:22 1997 +0200 +++ b/NEWS Mon Sep 29 15:39:28 1997 +0200 @@ -7,7 +7,7 @@ *** General Changes *** -* improved output of warnings / errors; +* improved output of warnings (###) / errors (***); * removed old README and Makefiles; @@ -15,7 +15,7 @@ conditional equations; * replaced print_goals_ref hook by print_current_goals_fn and - result_error_fn; +result_error_fn; * removed obsolete init_pps and init_database; @@ -25,9 +25,9 @@ *** Classical Reasoner *** -* Clarify_tac. clarify_tac, clarify_step_tac, Clarify_step_tac : - new tactics that use classical reasoning to simplify a subgoal - without splitting it into several subgoals; +* Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new +tactics that use classical reasoning to simplify a subgoal without +splitting it into several subgoals; * Safe_tac: like safe_tac but uses the default claset; @@ -55,22 +55,23 @@ are rewritten to `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)' -* HOL/Lists: the function "set_of_list" has been renamed "set" (and its - theorems too); +* HOL/Lists: the function "set_of_list" has been renamed "set" (and +its theorems too); *** HOLCF *** * HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases); -* added extended adm_tac to simplifier in HOLCF. Can now discharge - adm (%x. P (t x)), where P is chainfinite and t continuous. +* added extended adm_tac to simplifier in HOLCF -- can now discharge +adm (%x. P (t x)), where P is chainfinite and t continuous; *** FOL and ZF *** -* qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available. As - in HOL, they strip ALL and --> from proved theorems; +* qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as +in HOL, they strip ALL and --> from proved theorems; + New in Isabelle94-8 (May 1997)