Re: [isabelle] of/where with dummy-patterns



> >  thm imp_refl[of "undefined _ _"]
> >
> > inside a proof, this works fine. However, outside a proof, I get the
> > error message
> >  Duplicate fixed variable(s): "uu_"


Just for documentation: The (obvious) workaround is to write 
  thm imp_refl[of "undefined a b" for a b]

--
  Peter





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