Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

For the record: > Running on host lxbroy10 > isabelle: fc53fbf9fe01 tip > afp: 835c7e115feb tip > Running ConcurrentGC ... > Finished ConcurrentGC (1:08:48 elapsed time, 5:15:14 cpu time, factor 4.58) > 1:21:59 elapsed time, 5:53:13 cpu time, factor 4.30 This seems to be fine now.

Re: [isabelle-dev] popup in ce6320b9ef9b

>> Here is a minimal example, but I am at loss to explain what is going on >> here. > > The usual reason for a term being annotated twice is that it is (type) > checked twice. Good to know. Maybe a double-check somewhere in the interpretation machinery. Florian -- PGP available:

Re: [isabelle-dev] find_theorems and type class axioms

Hi all, > I had no idea that sort constraints played any role in the finding of > theorems, or why they should play a role. Whatever function they have in a > search doesn’t prevent the very similar query > > dist norm "op=“ > > from picking up quite a few things. To my mind it’s quite

Re: [isabelle-dev] find_theorems and type class axioms

> On 26 Nov 2015, at 11:58, Florian Haftmann > wrote: > > The sort constraints of constants play *no* role for > searching theorems. The sort constraints of terms to be searched *do*, > and in my view this is the desired behaviour: if I formulate a

Re: [isabelle-dev] find_theorems and type class axioms

Hi Larry, Type inferences assigns to "dist" the type "'a => 'a => real" where 'a :: metric_space, and to "norm" the type "'b => real" where 'b :: real_normed_vector (due to the type constraint manipulations in Real_Vector_Spaces.thy. The theorem dist_norm uses dist and norm with the sort

Re: [isabelle-dev] find_theorems and type class axioms

Ah, after I read Gerwin's email, I thought it was really a problem with find_theorems. But now you reminded me that it was the setup of dist_norm. As far as I remember the reason is that you want to have the syntactic type classes when you instantiate a type to have dist and norm. But later when

Re: [isabelle-dev] find_theorems and type class axioms

I still have no idea why find_theorems should refuse to find a theorem containing two named constants, no matter what the sorts say. Are there examples of searches that would deliver crazy results if this constraint were lifted? Larry > On 26 Nov 2015, at 14:41, Johannes Hölzl