Re: [isabelle] universal quantifiers vs. schematic variables

On 04.10.2015 20:24, Lars Hupel wrote:
> I don't have an insight into the early history of Isabelle. I have the
> understanding that the notion of schematic has been there for a long
> time. The only explanation I can offer is that schematic variables can
> be easily instantiated.

Schematic variables allow you to delay your choice of instantiation.
Moreover, they can be used to synthesize terms, which is regularly used
in program verification, e.g. to compute the weakest precondition of a
Hoare triple.

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