[opentheory-users] Importing from the Gilith OpenTheory Repo

[Ramana Kumar]

You can also use the -o or --output option instead of shell redirection.


On Sun, Nov 24, 2013 at 2:46 PM, Rob Arthan <rda at lemma-one.com> wrote:

> Ramana,
>
> On 24 Nov 2013, at 09:45, Ramana Kumar wrote:
>
> I think the idea of the base package is that everything in it should
> already be supported by your theorem prover, so you don't need to import it
> - rather, you use it as a dependency for things you export from your
> theorem prover.
>
> I want to import it so I can have a better look at it. The kind of thing I
> want to do is to make sure that my reader can prove all the assumptions in
> it and to make sure that my writer only uses definitions and theorems that
> it provides when it is writing out a ProofPower inference as a sequence of
> OpenTheory inferences.
>
> That said, I think you can generate a single article that performs all the
> proofs in a package, like base, using the opentheory tool with the info
> command and the --article option.
>
> I invoked opentheory like this:
>
> opentheory info --article base
>
> and after 12 minutes learnt that I should have invoked it like this:
>
> opentheory info --article base >base.art
>
> I am then able to import all 1117 theorems and 3 assumptions from base.art
> into ProofPower.
>
> Thanks!
>
> Rob.
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131124/c43f2c2e/attachment.html>