[isabelle-dev] Sledgehammer

[Amine Chaieb]

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 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? Sledgehammer will be in the upcoming release, so a 
> little testing can't hurt. I am quite fond of it since it proved
> 
> i div k = 0 <-> k=0 | 0 <= i < k | k < i <= 0
> 
> for me.
> 
> Tobias
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev