[Logiweb] rule

[Kasper H0st Frederiksen]

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