Re: [isabelle] What happens to ?thesis when there's a meta-for all quantifier?

You shouldn’t write a structured proof if the lemma statement includes meta-logical symbols in that way. Instead, try

  fixes x
  assumes “p x”
  shows “q x”
proof … qed


On 11 Jul 2014, at 23:07, Holden Lee <hl422 at> wrote:

> In the example, p and q are of type int==>bool. Contrast:
> lemma "⋀x. (p x)==>(q x)"
> proof -
> term ?thesis (*"q":: "int ⇒ bool"*)
> show ?thesis sorry
> qed

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