Re: [isabelle] conservativity of HOL constant and type definitions



And here you don't have an existential
quantifier for type constructors so you can use the approach as you did
for constants.

should have been: ... you cannot use the approach as you did
for constants.





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