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



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

(*
Type unification failed: Clash of types "_ ⇒ _" and "bool"

Type error in application: incompatible operand type

Operator:  Trueprop :: bool ⇒ prop
Operand:   ?thesis :: int ⇒ bool
*)

*is not OK* (I'm mystified as to why ?thesis is "q".) but

lemma "p x==>q x"
proof -
term ?thesis (* "q x":: "bool" *)
show ?thesis sorry
qed

is OK.

In the first case, what should I replace ?thesis by to make it correct
(other than the whole statement in quotes)?

Thanks,
Holden



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