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
assumes “p x”
shows “q x”
proof … qed
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and