[Logiweb] rule

[Martin Røpcke]

Oh yes, now I remember. Thanks.
Martin

On Fri, 1 Jul 2005, Kasper H0st Frederiksen wrote:

> Remember that you can only add a axiom to a theory that is defined on the 
> same page. If you are using a reference to the peano page, like me, then you 
> can't add new axioms.
>
> -Kasper Frederiksen
>
>
> On Thu, 30 Jun 2005, Martin Røpcke wrote:
>
>> If I would like to state a rule and use it in another proof how do I do 
>> this? I remember that either Klaus said something about it or I have read 
>> about it somewhere. I tried with:
>> 
>> "[math in theory system prime s
>> rule mendelson proposition three two h g ii
>> says
>> .
>> .
>> .
>> end rule
>> end math ]"
>> 
>> But I get an error saying "the theory does not assert this rule". I can 
>> state it as a lemma, and I'm pretty sure it's valid, though I havn't 
>> proved it yet. The lemma/rule is:
>> 
>> x' + y = (x + y)' |- y' + x = (y + x)'
>> 
>> I believe this should be provable.
>> 
>> Regards,
>> Martin
>> _______________________________________________
>> Logiweb mailing list
>> Logiweb at diku.dk
>> http://miming.diku.dk/mailman/listinfo/logiweb
>> (Web access from inside DIKUs LAN only)
>> 
>> 
>
>
>

Mvh
Martin

"I'm a great believer in luck and I find the harder I work,
the more I have of it."
                                            Thomas Jefferson
-------------- next part --------------
_______________________________________________
Logiweb mailing list
Logiweb at diku.dk
http://miming.diku.dk/mailman/listinfo/logiweb
(Web access from inside DIKUs LAN only)