<div dir="ltr">Dear Günter,<br><br>I can answer some but not all of your questions, and do so below.<br><div><div class="gmail_extra"><br><div class="gmail_quote">On 14 August 2015 at 00:15, Günter Rote <span dir="ltr"><<a href="mailto:rote@inf.fu-berlin.de" target="_blank">rote@inf.fu-berlin.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">When opentheory processes a theory, does it read all theory article files<br>
on which it depends?<br></blockquote><div><br></div><div>opentheory would need to know the logical content (the theory inputs and outputs) of the dependencies, in order to calculate the theory inputs and outputs of the theory being processed. Whether it figures these out by processing the dependencies or using some caches, I'm not sure.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Or is there a way that it just needs to read the theorems from<br>
other packages that it uses?<br></blockquote><div><br></div><div>I suspect there is a cache, but Joe would know.<br></div><div> <br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

I can somehow guess what the entry<br>
  show: "Data.Bool"<br>
in the .thm file means, but it is not completely clear.<br>
In particular, what happens when there are several "show: " lines?<br></blockquote><div><br></div><div>Each "show: " line adds another bit of namespace that won't need to be printed. I agree that their exact format and effect is a bit mysterious, though.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

Is there a way to eventually look at the theorems that are proved<br>
in detail in an unambiguous format with all type information? (other than the html<br>
format with mouse-over?)<br></blockquote><div><br></div><div>I would say that the article itself is this "unambiguous format". If you want to see a term in any other format, you can write an article parser that will build the term and then print it however you like.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Best regards :<br>
<span><font color="#888888">--<br>
G"unter Rote               (Germany=49)30-838-75150 (office)<br>
Freie Universit"at Berlin                    -75103 (secretary)<br>
Institut f"ur Informatik       FAX (49)30-838-75192<br>
Takustrase 9, D-14195 Berlin, GERMANY<br>
<br>
<br>
</font></span><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div></div></div>