On Tue, 3 Feb 2004, Freek Wiedijk wrote: > >2. Blocks that in a 'per cases' reasoning end with an 'end'. > > So now it's possible to "nest" per cases without a "proof end"? Yes, that's the plan, but still there are some errors to be fixed and Czeslaw is working on them at the moment. It's one of the reasons why we haven't decided to put version 7 for official distribution yet. Adam Naumowicz