[ProofPower] type variables in subgoal package

[Philip Clayton]

Roger Bishop Jones wrote:

>In relation to your comments to Steve about losing
>the assumptions on things you strip into the assumptions,
>this is not correct.
>

I didn't mean losing in that sense.  If you put the theorem |- A into 
the assumptions of the subgoal B ?|- C you get the subgoal A, B ?|- C 
--- exactly the same as if the theorem B |- A had been added to the 
assumptions of B ?|- C. Clearly |- A is a stronger theorem than  B |- A 
but adding either to the subgoal B ?|- C has the same effect.  In that 
sense, some information has been lost.  (In particular, the subgoal 
package did not record the fact the |- A is independent of all other 
assumptions, whereas B |- A is not.)

Phil