On Mon, 19 Jan 2015, Jasmin Blanchette wrote:
Just a reminder that this old thread is not yet resolved and currently
I'm essentially stuck.
I hope somebody who has a clue will answer your email.
I still have various important markers on this mail thread, to see if I
can tell something
Hi Chris,
Just a reminder that this old thread is not yet resolved and currently I'm
essentially stuck.
I hope somebody who has a clue will answer your email.
Independent of my being stuck, could one of the devs apply at least the first
of the following attached patches (and the second
Just a reminder that this old thread is not yet resolved and currently
I'm essentially stuck.
Independent of my being stuck, could one of the devs apply at least the
first of the following attached patches (and the second one depending on
whether dropping semicolons is in general seen as good
Cf. http://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e
Dmitriy
On 23.11.2014 21:20, Christian Sternagel wrote:
*Moved from isabelle-users*
Thanks for the crucial hint Dmitriy!
Coming back to the original issue of Andreas, some explanation might
be in order.
What we did until
Thanks again Dmitriy,
it seems that my fix was too quick. Since sending my email yesterday I
worried already whether doing unification inside adhoc_overloading.ML is
such a good idea (since the unifier might inject schematic type
variables stemming from the internal generic theory data of
*Moved from isabelle-users*
Thanks for the crucial hint Dmitriy!
Coming back to the original issue of Andreas, some explanation might be
in order.
What we did until now in adhoc_overloading.ML (more precisely, the
function insert_variants) was to check for a given constant c of
type T
