Re: [isabelle] tactic being executed twice



On 05/06/18 17:17, Jeremy Dawson wrote:
> 
> What I'm doing right now is trying to code up an absurdly trivial
> example of a tactic which should succeed using an absurdly trivial
> oracle, which isn't included in the code I showed, but fails in the same
> way (at least, the same, in that the tactic gets applied to a goal which
> does not have the requisite number of subgoals).

Just some guesses from a long distance:

  * there is something wrong with the goal context (type Proof.context)

  * type-inference has produced unexpectedly general results (usually
due to a wrong context)


	Makarius




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