Re: [isabelle] The Incredible Proof Machine
-----BEGIN PGP SIGNED MESSAGE-----
Sorry, I really can't remember the details, but I'm pretty sure that
it was just about the concrete implementation of the "devar" function
(section 6; so it should not be related to section 9).
I hope that Julian will fill in the details at some point ;)
On 09/25/2015 12:33 PM, Joachim Breitner wrote:
> Dear Christian,
> Am Freitag, den 25.09.2015, 11:13 +0200 schrieb Christian
>> 2) Since you mentioned the nice paper by Tobias (on higher-order
>> pattern unification). Did you also implement the "devar"
>> optimization of the same paper? Just recently, Julian Nagele (a
>> PhD student in our group; who I also CC'ed), stumbled upon a
>> problem with "devar" when implementing the same algorithm. I do
>> not remember the details (maybe Julian could comment), only that
>> a little bit of hg-digging revealed the following changeset:
>> changeset: 12232:ff75ed08b3fb user: berghofe date:
>> Mon Nov 19 17:34:02 2001 +0100 summary: Replaced devar by
>> (referring to src/Pure/pattern.ML)
>> I'm curios to whether others already had a similar experience
>> with "devar" and what the intention behind this change was?
> Are you referring to âÂ9 Minimizing new variablesâ in the paper?
> Since this seems to be part of the ML code in
> http://www21.in.tum.de/~nipkow/pubs/lics93-alpha.ML which I based
> my implementation on, I also have that. If there is anything wrong
> with it, Iâd like to know of course!
> Thanks, Joachim
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2
-----END PGP SIGNATURE-----
This archive was generated by a fusion of
Pipermail (Mailman edition) and