Re: [isabelle] Converting fixed variables to ?-wildcards



Peter Lammich wrote:

Is there a way to the fixed variables replaced by wildcards, but not getting this locale-assumption in front of the lemma (of course, without retyping and proving the special version of the lemma ;) ) ?

Regards,
 Peter


Peter,

I've never tried doing this inside a locale, but, to turn free variables into ?-variables,
without doing the other stuff that standard does,  I have used

(gen_all o forall_intr_frees), thus

val mp' = "[| P --> Q; P |] ==> Q" : Thm.thm
> (gen_all o forall_intr_frees) mp';
val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : Thm.thm

Jeremy






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