See now http://isabelle.in.tum.de/reports/Isabelle/rev/7f990b3d5189
which seems to do the job. There a still dark corners wrt. to base sort
inference which maybe one day will lift its ugly head but for the moment
it is OK.
Florian
On 10.09.2014 10:35, Florian Haftmann wrote:
Hi
On 11/09/2014 14:05, Jasmin Christian Blanchette wrote:
Hi all,
It appears that the Sum of Squares server is down. This makes the build of
the HOL-Library session diverge, at least on my machine, when
ISABELLE_FULL_TESTS is enabled. In addition, it appears to be at the source
of the
I have installed a copy of the software locally. Would be worth making this a
component?
--lcp
On 11 Sep 2014, at 13:07, Tobias Nipkow nip...@in.tum.de wrote:
On 11/09/2014 14:05, Jasmin Christian Blanchette wrote:
Hi all,
It appears that the Sum of Squares server is down. This
Hi Florian,
Am 10.09.2014 um 10:22 schrieb Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de:
when we started this hook business, the situation was as follows:
a) Hook clients were all for adding type class instances, i.e.
inherently working a the theory level.
b) Hooks were a
