proper handling of dangling sort hypotheses (at last!);
authorwenzelm
Wed Sep 29 14:36:36 1999 +0200 (1999-09-29)
changeset 76472ceddd91cd0a
parent 7646 1ad3866b86cc
child 7648 8258b93cdd32
proper handling of dangling sort hypotheses (at last!);
NEWS
     1.1 --- a/NEWS	Wed Sep 29 14:36:04 1999 +0200
     1.2 +++ b/NEWS	Wed Sep 29 14:36:36 1999 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4  	mk_solver: string -> (thm list -> int -> tactic) -> solver
     1.5  where the string argument is only a comment.
     1.6  
     1.7 +
     1.8  *** Proof tools ***
     1.9  
    1.10  * Provers/Arith/fast_lin_arith.ML contains a functor for creating a
    1.11 @@ -288,6 +289,12 @@
    1.12  your own database of information attached to *whole* theories -- as
    1.13  opposed to intra-theory data slots offered via TheoryDataFun;
    1.14  
    1.15 +* proper handling of dangling sort hypotheses (at last!);
    1.16 +Thm.strip_shyps and Drule.strip_shyps_warning take care of removing
    1.17 +extra sort hypotheses that can be witnessed from the type signature;
    1.18 +the force_strip_shyps is gone, any remaining shyps are simply left in
    1.19 +the theorem (with a warning issued by strip_shyps_warning);
    1.20 +
    1.21  
    1.22  
    1.23  New in Isabelle98-1 (October 1998)