[opentheory-users] format of opentheory parameters

[Joe Leslie-Hurd]

[cc'ing the opentheory mailing list]

Hi Gunter,

> INPUT is one of the following:
>   - A package: NAME-VERSION or NAME (for the latest version)
>   - A theory source file: FILE.thy or theory:FILE
>   - ...

What this meant to say (and I agree it's not crystal clear) is that if
the file has an extension .thy it will be treated by default as a
theory file, but you can treat any other file as a theory file by
prepending theory: to the name of the file. So if you have a theory
file two_c.thy you can process it just using

opentheory info two_c.thy

but if you have a theory file called two_c.txt then you will need to
prepend theory: for the opentheory tool to properly interpret it:

opentheory info theory:two_c.txt

>>opentheory info two_c.thy
> triggers
> opentheory: unknown type of input: two_c.thy

In the light of the above, this error is very strange. What platform are you on?

Cheers,

Joe