Does anybody know why the runtime of HOL-NumberTheory has doubled
recently? (See http://isabelle.in.tum.de/devel/stats/at-poly.html)
Makarius
Ich will es auch dem naechst intallieren um folgendes zu beweisen:
Ifm (rqe p) bs = Ifm p bs /\ qfree (rqe p)
Hoffentlich klappt es :)
Aemin.
Tobias Nipkow wrote:
>> We need people to play with sledgehammer
>> (anybody doing big proofs at TUM just now?) and to suggest what settings
>> to prov
> We need people to play with sledgehammer
> (anybody doing big proofs at TUM just now?) and to suggest what settings
> to provide. Currently I envisage selection of prover and full proofs.
> Possibly tweaks to the relevance filter (to tighten or loosen it) may be
> useful.
Any guinea-pigs? Sl
