[Logiweb] Error with the new base page

[Kasper H0st Frederiksen]

You are right. I am now using both the newest base _and_ peano pages:

BIBLIOGRAPHY
base: 
"http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-22-UTC-06-58-05-413682/vector/page.lgw",
peano: 
"http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/vector/page.lgw"

my claims are succeding now.

-Kasper Frederiksen


On Wed, 22 Jun 2005, Klaus Ebbe Grue wrote:

> 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
> 
>