Re: [Rodin-b-sharp-user] Prover preferences

[Nicolas B. <nic...@sy...>]

Hello Ken,

It's nothing related to prover configuration, but rather a missing proof 
command.
This problem has been addressed in the Rodin 1.3, which will be released 
on April 30th: there will be a new right-click command in the explorer 
that launches the auto provers on undischarged POs. That will make 
things quite easier :)

Cheers,

Nicolas

Ken Robinson a écrit :
> I'm noticing two things that I assume imply that my prover preferences are not set correctly.
>
> 1 when I load, say, the first undischarged PO and then sequence through undischarged PO in the proof control windows, it is not uncommon for quite a few ---sometimes all--- of the POs to be discharged
>
> 2 (probably related to 1) I am finding that some undischarged POs are discharged by ml without any further actions on my part.
>
> I've got ml in both auto and post tactics.
>
> Is there anything else I can do save the apparently unnecessary steps to go through the above?
>
> Thanks for any help or pointers.
>
> Cheers,
>
> Ken
> ------------------------------------------------------------------------------
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
> ---------------------------------------------------------------------------------------
> Orange vous informe que cet  e-mail a ete controle par l'anti-virus mail. 
> Aucun virus connu a ce jour par nos services n'a ete detecte.
>
>
>
>   

-- 
------------------------------------------------------------------------
Nicolas BEAUGER                           Tél. : (+33)(0)4 42 90 65 66
Ingénieur Logiciel

SYSTEREL
------------------------------------------------------------------------
Standard / Fax : (+33)(0)4 42 90 41 20 / 29     site : www.systerel.fr
------------------------------------------------------------------------