Re: [isabelle] how to eliminate ALL
I have this lemma in the format "[| A; B |] ==> ALL x. C x". I want to
apply allI to the rule to get rid of the ALL before applying it with
apply (rule ...), which ought to be a simple task. I was thinking it
would be something like apply (rule myLemma[THEN/OF allI]).
apply (rule myLemma[THEN spec])
allI is what you do on goals, but on facts you need elimination.
This archive was generated by a fusion of
Pipermail (Mailman edition) and