Re: [isabelle] dest_Trueprop question

Thanks Jeremy, Makarius for the advice. Useful to know.

For the dest_Trueprop issue, it is the 'auto' step that causes
the TERM exception. To be concrete I have put a small theory file at:

which demonstrates what is happening

Makarius wrote:
> ...
> Is this caused by induct or auto?  Sometimes a meta-level quantifier gets
> a more general type than expected (e.g. 'a::{}).  Then certain tools fail
> to internalize a problem into the object-logic.
> 	Makarius

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