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

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

Larry

On 11 Jul 2014, at 23:07, Holden Lee <hl422 at cam.ac.uk> 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.