Re: [isabelle] dest_Trueprop question



This looks like a bug. Please send me a theory file, preferably the smallest possible that causes this behaviour.

Larry Paulson


On 16 Jun 2006, at 19:26, Dimitrios Vytiniotis wrote:

I have an inductive relation and some of the inference rules
use meta-level quantifiers on the premises.
I found that more convenient because at use sites it is easier
for me to instantiate these things than when using object-level
quantifiers.

I very often in my development use the style:

lemma blabla: ...
  by(induct X, auto elim: MyRelation.elims)

And although I feel it should work, I get back the error:
   *** exception TERM raised: dest_Trueprop






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