|
Changes
- tuning
(detail / hgweb)
- tuned NEWS
(detail / hgweb)
- compile HOL-TPTP
(detail / hgweb)
- compile Metis_Examples
(detail / hgweb)
- more NEWS
(detail / hgweb)
- compile mirabelle
(detail / hgweb)
- tweaked Auto Sledgehammer's behavior and output
(detail / hgweb)
- updated NEWS
(detail / hgweb)
- removed experimental prover z3_tptp
(detail / hgweb)
- print more verbose information
(detail / hgweb)
- run all installed provers by default
(detail / hgweb)
- update slice options centrally
(detail / hgweb)
- further work on new Sledgehammer slicing
(detail / hgweb)
- tweaked verbose output
(detail / hgweb)
- tweak padding of prover slice schedule to include all provers
(detail / hgweb)
- implemented 'max_proofs' mechanism
(detail / hgweb)
- document new option 'max_proofs'
(detail / hgweb)
- crude implementation of centralized slicing
(detail / hgweb)
- removed obscure E option
(detail / hgweb)
- take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
(detail / hgweb)
- rationalize slicing format
(detail / hgweb)
- thread slices through
(detail / hgweb)
- simplified 'best_slice' data structure and made minor changes to slices
(detail / hgweb)
- changed logic of 'slice' option to 'slices'
(detail / hgweb)
- updated documentation of 'slice' (now 'slices') option
(detail / hgweb)
- revised Sledgehammer documentation
(detail / hgweb)
- rationalized output for forthcoming slicing model
(detail / hgweb)
- use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
(detail / hgweb)
- disable slicing within ATP module (in preparation for refactoring)
(detail / hgweb)
- disable slicing within SMT (in preparation for factoring it out)
(detail / hgweb)
- generalized the 'slice' option towards more flexible slicing
(detail / hgweb)
|
![[Jenkins]](/jenkins/static/98dcae99/images/svgs/logo.svg){kind=logo}
