Re: [isabelle] dest_Trueprop question
This looks like a bug. Please send me a theory file, preferably the
smallest possible that causes this behaviour.
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
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