Re: [isabelle] Odd failure to match local statement with pending goal.



Hi,

> As Larry stated, this is indeed a strange problem. I tried to find a
> minimal example; here is what I came up with:
> 
> -------------------
> lemma
>   shows  "⋀c d. d ∈ Z ⟹ x = c ⟹
>         ∃e. e ∈ {_. ∃e. e ∈ Z ∧ y = e}"
>   apply (unfold mem_Collect_eq)
> proof -
>   fix s t
>   assume "x = s" and "t ∈ Z"
>   then show "∃s t. t ∈ Z ∧ y = t"
>     sorry
> qed
> -------------------
> The show statement fails with
[...]

So do we know whether this is an obscure feature or possibly a bug?
(If it's a feature I'd love to hear the underlying story.)

Best regards,

Bertram





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