I’m not sure what the question is any more. If it is about the choice of names
in Skolemization, that has been entirely redone in the past few years. I
imagine it is now something like this:
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
EVERY1 [skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt'])
ctxt 1]) i st
(I found this in meson.ML.)
The original version made little use of contexts, as I recall.
Larry
On 12 Feb 2014, at 20:23, Jasmin Blanchette <[email protected]> wrote:
> Am 12.02.2014 um 20:40 schrieb Makarius <[email protected]>:
>
>> Mainly the proof reconstruction on the Isabelle side, especially the
>> question of type variables.
>
> I can't help much there. Perhaps Larry knows more. All I can recall is that
> Metis sometimes suggests type instantiations (since types are encoded as
> terms, and type variables as term variables), but that in "metis" these are
> ignored for some reason, sometimes leading to more polymorphic theorems on
> the Isabelle side of things than on the Metis side.
>
> Jasmin
>
> _______________________________________________
> isabelle-dev mailing list
> [email protected]
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
