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:

  http://www.cis.upenn.edu/~dimitriv/poplmark/Simple.thy

which demonstrates what is happening
thanks!
-d


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.