[isabelle] Free variables vs schematic variables



Hi,

Just a quick question: how come Isabelle keeps a distinction between free
and schematic variables? It seems that free variables in a goal are
converted to schematic anyway, so what are the benefits of keeping them
distinct?

Cheers
Steve




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