<div dir="ltr">Hi Rob,<div><br></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">What I was rather hoping was that I could substitute for the definitions and axioms and then import the proofs of the theorems. If I import say pair-thm, I find it involves a lot more assumptions other than definitions. I would have hoped that the assumptions in pair-thm would just be:<br>

<br>
!xy?x y. xy = (x, y)<br>
<br>
!x y. fst(x, y) = x<br>
<br>
!x y. snd(x, y) = y<br></blockquote><div><br></div><div>When I look at the assumptions of my (perhaps more recent) pair-thm theory, it has 46 assumptions, but the 3 you list above are the only ones that refer to pair type operators and constants. The rest are theorems exported by the bool package.</div>
<div><br></div><div>So if you replace the 3 pair-def theorems with ProofPower versions, and also have all the theorems from the bool theory available, then you can prove all the theorems in pair-thm. In this way you can build up all the theorems from the standard library by just replacing the *-def theorems with ProofPower versions, processing the proofs of theorems in other packages and storing them to satisfy assumptions of later packages.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div></div></div></div>