Re: [isabelle] how to eliminate ALL



Hi Chris,

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]).

Try

   apply (rule myLemma[THEN spec])

allI is what you do on goals, but on facts you need elimination.


Alex






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