[isabelle-dev] HOL-IMP very slow

[Lawrence Paulson]

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 <jasmin.blanchette at gmail.com> wrote:

> Am 12.02.2014 um 20:40 schrieb Makarius <makarius at sketis.net>:
> 
>> 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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev