equal
deleted
inserted
replaced
33 setSSolver addSSolver setSolver addSolver |
33 setSSolver addSSolver setSolver addSolver |
34 is now simpset * solver -> simpset where `solver' is a new abstract type |
34 is now simpset * solver -> simpset where `solver' is a new abstract type |
35 for packaging solvers. A solver is created via |
35 for packaging solvers. A solver is created via |
36 mk_solver: string -> (thm list -> int -> tactic) -> solver |
36 mk_solver: string -> (thm list -> int -> tactic) -> solver |
37 where the string argument is only a comment. |
37 where the string argument is only a comment. |
|
38 |
38 |
39 |
39 *** Proof tools *** |
40 *** Proof tools *** |
40 |
41 |
41 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a |
42 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a |
42 decision procedure for linear arithmetic. Currently it is used for |
43 decision procedure for linear arithmetic. Currently it is used for |
285 |
286 |
286 * theory loader actions may be traced via new ThyInfo.add_hook |
287 * theory loader actions may be traced via new ThyInfo.add_hook |
287 interface (see src/Pure/Thy/thy_info.ML); example application: keep |
288 interface (see src/Pure/Thy/thy_info.ML); example application: keep |
288 your own database of information attached to *whole* theories -- as |
289 your own database of information attached to *whole* theories -- as |
289 opposed to intra-theory data slots offered via TheoryDataFun; |
290 opposed to intra-theory data slots offered via TheoryDataFun; |
|
291 |
|
292 * proper handling of dangling sort hypotheses (at last!); |
|
293 Thm.strip_shyps and Drule.strip_shyps_warning take care of removing |
|
294 extra sort hypotheses that can be witnessed from the type signature; |
|
295 the force_strip_shyps is gone, any remaining shyps are simply left in |
|
296 the theorem (with a warning issued by strip_shyps_warning); |
290 |
297 |
291 |
298 |
292 |
299 |
293 New in Isabelle98-1 (October 1998) |
300 New in Isabelle98-1 (October 1998) |
294 ---------------------------------- |
301 ---------------------------------- |