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

author | paulson |

Wed, 24 Jun 1998 10:33:42 +0200 | |

changeset 5075 | 9a3d48fa28ca |

parent 5074 | 753d4daff1df |

child 5076 | fbc9d95b62ba |

removed duplicate entry for Goal

--- a/NEWS Wed Jun 24 10:30:29 1998 +0200 +++ b/NEWS Wed Jun 24 10:33:42 1998 +0200 @@ -7,9 +7,14 @@ *** General Changes *** -* Simplifier: +* new toplevel commands `Goal' and `Goalw' that improve upon `goal' +and `goalw': the theory is no longer needed as an explicit argument - +the current theory is used; assumptions are no longer returned at the +ML-level unless one of them starts with ==> or !!; it is recommended +to convert to these new commands using isatool fixgoal (as usual, +backup your sources first!); - -Asm_full_simp_tac is now more aggressive: +* Simplifier: Asm_full_simp_tac is now more aggressive. 1. It will sometimes reorient premises if that increases their power to simplify. 2. It does no longer proceed strictly from left to right but may also @@ -29,25 +34,12 @@ delWrapper, delSWrapper: claset * string -> claset getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; -* new toplevel commands `Goal' and `Goalw' that improve upon `goal' and -`goalw': the theory is no longer needed as an explicit argument - the current -theory is used; assumptions are no longer returned at the ML-level unless one -of them starts with ==> or !!. It is recommended to convert to these new -commands. - * inductive definitions now handle disjunctive premises correctly (HOL and ZF); * new toplevel commands 'thm' and 'thms' for retrieving theorems from the current theory context; -* new toplevel commands `Goal' and `Goalw' that improve upon `goal' -and `goalw': the theory is no longer needed as an explicit argument - -the current theory is used; assumptions are no longer returned at the -ML-level unless one of them starts with ==> or !!; it is recommended -to convert to these new commands using isatool fixgoal (as usual, -backup your sources first!); - * new theory section 'nonterminals'; * new theory section 'setup';