Re: [isabelle] Instantiation problem


It follow from a simple instantiation ( i <-- (cinc i) ) but I don't find
how to help Isabelle to execute it and using normal proof methods Isabelle
don't find the solution.

try the following :

apply (rule_tac x="cinc i" in exI)

The x comes from the name of the free variable in the rule exI

thm exI

For more details, see section 5.9.6 of the Isabelle tutorial.


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