Re: [isabelle] Free variables vs schematic variables

On Wed, 13 Jun 2012, Ramana Kumar wrote:

as I understand it, the distinction is fundamentally unavoidable because one kind of variable is in the object-logic syntax and the other is a meta-logic variable.

Both free and schematic variables belong to Isabelle/Pure, just like bound variables via !!x or %x. You could argue if Isabelle/HOL has actually variables on its own -- it just re-uses many things from Pure directly, including the type system, for example.


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