[isabelle] strange tvar


  In examining the proof of HOL.less_max_iff_disj I came upon something
I found strange, which indicates I don't understand this aspect of the proof term:

In all the other proofs I've seen up to this point (and I've seen hundreds), all the free TVars were contained in the conclusion or premises of the theorem. Moreover, all of these
TVars had index 0 (as part of the "indexname" type) In this case,
there is a free TVar deep in the proof "'t" with index "111". Now I have no idea where this came from, nor the significance of the index, especially
such a seemingly strange one as this.

Can anyone explain what is going on here? I thought the index was just for some
nonlogical optimization.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.