[isabelle-dev] [isabelle] match_tac, schematic and bound variables
makarius at sketis.net
Mon Aug 19 22:55:00 CEST 2013
On Sun, 18 Aug 2013, Lars Noschinski wrote:
>> Combinators like Subgoal.FOCUS have replaced a lot of old-style
>> tinkering with goals; within the focused parts things are fixed and
>> don't get instantiated by accident.
> I seem to remember a discussion on the mailing list that Subgoal.FOCUS
> does not export schematic type variables. So this would give us another
> not-quite correct match implementation.
I still have this on my list to look after it in further detail, but as
far as I can tell it was about situations that are conceptially not
allowed anyway: schematic type variables within fixed-term variables.
The inference kernel happens to allow that in primitive rules, but almost
everything will break down. Type-inference is part of the syntactic
phase, and needs to be finished before doing the actual logical
More information about the isabelle-dev