Re: [Rodin-b-sharp-user] Proof Skeleton & Simlify Proofs

[Ken R. <ke...@cs...>]

˙Hi Matthias,

On 09/10/2009, at 19:45 PM, Matthias Schmalz wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Hi,
>
> first of, I appreciate the proof skeleton view and the simplify proofs
> function.
>
> Now my questions:
> 1.
> Sometimes, the proof skeleton view does not display the current proof.
> Steps to reproduce the problem (in Rodin 1.0):
> 1. Open some proof. (e.g. the proof in the attached archive)
> 2. Open the proof skeleton view as a fast view.
> 3. The proof skeleton view just contains "no proof to display".
>
> Maybe I misunderstand which proof should be displayed in the proof
> skeleton view.

Yes, it's a bit confusing isn't it? :-)

What you need to do is to highlight the proof obligation in the Event- 
B explorer and then select the proof skeleton and you should see the  
proof.

Cheers,

Ken