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

author | paulson |

Thu, 25 Sep 1997 13:23:41 +0200 | |

changeset 3715 | 6e074b41c735 |

parent 3714 | ab3b4ceb61dc |

child 3716 | 2885b760a4b4 |

Clarify_tac; general reorganization

--- a/NEWS Thu Sep 25 12:32:14 1997 +0200 +++ b/NEWS Thu Sep 25 13:23:41 1997 +0200 @@ -5,16 +5,49 @@ New in Isabelle???? (DATE ????) ------------------------------- -* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; +*** General Changes *** + +* improved output of warnings / errors; -* HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases); +* removed old README and Makefiles; -* added extended adm_tac to simplifier in HOLCF. Is now capable to discharge - adm (%x. P (t x)), where P is chainfinite and t continuous. +* defs may now be conditional; improved rewrite_goals_tac to handle +conditional equations; * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn; +* removed obsolete init_pps and init_database; + +* deleted the obsolete tactical STATE, which was declared by + fun STATE tacfun st = tacfun st st; + + +*** 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; + + +*** Simplifier *** + +* added simplification meta rules: + (asm_)(full_)simplify: simpset -> thm -> thm; + +* simplifier.ML no longer part of Pure -- has to be loaded by object +logics (again); + +* added prems argument to simplification procedures; + + +*** Syntax *** + +* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; + + +*** HOL *** + * HOL/simplifier: terms of the form `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) are rewritten to @@ -23,25 +56,13 @@ * HOL/Lists: the function "set_of_list" has been renamed "set" (and its theorems too); -* removed old README and Makefiles; -* removed obsolete init_pps and init_database; - -* defs may now be conditional; improved rewrite_goals_tac to handle -conditional equations; - -* improved output of warnings / errors; +*** HOLCF *** -* deleted the obsolete tactical STATE, which was declared by: - fun STATE tacfun st = tacfun st st; +* HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases); -* added simplification meta rules: - (asm_)(full_)simplify: simpset -> thm -> thm; - -* simplifier.ML no longer part of Pure -- has to be loaded by object -logics (again); - -* added prems argument to simplification procedures; +* added extended adm_tac to simplifier in HOLCF. Can now discharge + adm (%x. P (t x)), where P is chainfinite and t continuous.