On Mon, Sep 30, 2013 at 2:34 PM, Makarius <makar...@sketis.net> wrote: > According to the normal context discipline, free variables are always fixed, > like a local const. We have a few tools that violate that principle and > consequently cause confusion, e.g. the Simplifier. There are sometimes > historical reasons for that, and little hope for reforms. > > Is this also the case for transfer?
If you're asking whether transfer distinguishes the term constructors Free and Const, then the answer is yes. Transfer may generalize a Free (according to the heuristic) but will never generalize over a Const. With more and more localized tools using Frees as constants, perhaps it would be more robust for transfer to treat Free and Const exactly the same. I will have to think more about this. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
