[Logiweb] Error with the new base page

[Klaus Ebbe Grue]

Hi Kasper,

> I just updated my base page reference from:
> http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-03-UTC-15-49-33-495567/vector/page.lgw
>
> to:
> http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-22-UTC-06-58-05-413682/vector/page.lgw
>
> This is the only change. Now i get a "claim failed"
> and a diagnose
> "Lemma expected S1'" in one of my proofs that use S1'.

I remember I got the same error myself. And that the message made complete 
sense *after* I spotted the problem. I will try to remember what the 
problem was, but quite likely it was on the old "peano" page.

The new "peano" page is called "peano" instead of "peano axioms". Changing 
to the new "peano" page might solve the problem (but may create new ones 
since I have defined new constructs on the new peano page which will 
conflict if you happen to have defined constructs with the same name).

It is of course always an option to stay with the old base page. The only 
problems with that are:
(1) The old unification tactic may produce variable clashes.
(2) Proof lines that make local macro definitions are rendered off-margin.
(3) Proof lines that assume side-conditions are slightly off-margin.

Klaus