removed duplicate entry for Goal
authorpaulson
Wed Jun 24 10:33:42 1998 +0200 (1998-06-24)
changeset 50759a3d48fa28ca
parent 5074 753d4daff1df
child 5076 fbc9d95b62ba
removed duplicate entry for Goal
NEWS
     1.1 --- a/NEWS	Wed Jun 24 10:30:29 1998 +0200
     1.2 +++ b/NEWS	Wed Jun 24 10:33:42 1998 +0200
     1.3 @@ -7,9 +7,14 @@
     1.4  
     1.5  *** General Changes ***
     1.6  
     1.7 -* Simplifier:
     1.8 +* new toplevel commands `Goal' and `Goalw' that improve upon `goal'
     1.9 +and `goalw': the theory is no longer needed as an explicit argument -
    1.10 +the current theory is used; assumptions are no longer returned at the
    1.11 +ML-level unless one of them starts with ==> or !!; it is recommended
    1.12 +to convert to these new commands using isatool fixgoal (as usual,
    1.13 +backup your sources first!);
    1.14  
    1.15 - -Asm_full_simp_tac is now more aggressive:
    1.16 +* Simplifier: Asm_full_simp_tac is now more aggressive.
    1.17    1. It will sometimes reorient premises if that increases their power to
    1.18       simplify.
    1.19    2. It does no longer proceed strictly from left to right but may also
    1.20 @@ -29,25 +34,12 @@
    1.21    delWrapper, delSWrapper: claset *  string            -> claset
    1.22    getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
    1.23  
    1.24 -* new toplevel commands `Goal' and `Goalw' that improve upon `goal' and
    1.25 -`goalw': the theory is no longer needed as an explicit argument - the current
    1.26 -theory is used; assumptions are no longer returned at the ML-level unless one
    1.27 -of them starts with ==> or !!. It is recommended to convert to these new
    1.28 -commands.
    1.29 -
    1.30  * inductive definitions now handle disjunctive premises correctly (HOL
    1.31  and ZF);
    1.32  
    1.33  * new toplevel commands 'thm' and 'thms' for retrieving theorems from
    1.34  the current theory context;
    1.35  
    1.36 -* new toplevel commands `Goal' and `Goalw' that improve upon `goal'
    1.37 -and `goalw': the theory is no longer needed as an explicit argument -
    1.38 -the current theory is used; assumptions are no longer returned at the
    1.39 -ML-level unless one of them starts with ==> or !!; it is recommended
    1.40 -to convert to these new commands using isatool fixgoal (as usual,
    1.41 -backup your sources first!);
    1.42 -
    1.43  * new theory section 'nonterminals';
    1.44  
    1.45  * new theory section 'setup';