[isabelle-dev] find_theorems and type class axioms

Andreas’s message reminds me that axioms of type classes are still not picked up: class dist_norm = dist + norm + minus + assumes dist_norm: "dist x y = norm (x - y)” This item has the status of a theorem. However, the query dist "norm(_-_)” doesn’t find it. Surely it should? Larry

Re: [isabelle-dev] CGSCreateKeyboardEvent

My impression is that this message appears after quitting Isabelle under unusual circumstances, e.g., after it asks you what to do with a modified buffer. I am using OS X El Capitan. Larry > On 15 Nov 2015, at 21:37, Makarius wrote: > > Larry, > > I am forwarding this

[isabelle-dev] extra lemmas

Can someone add these in at the obvious places? thanks, peter lemma LeastI2_wellorder_ex: assumes "\x::'a::wellorder. P x" and "\a. \ P a; \b. P b \ a \ b \ \ Q a" shows "Q (Least P)" using assms by clarify (blast intro!: LeastI2_wellorder) lemma fcomp_comp: "fcomp f g = comp g f" by

Re: [isabelle-dev] the function "real"

On 12.11.2015 13:58, Lars Noschinski wrote: > On 11.11.2015 22:09, Johannes Hölzl wrote: >> It looks like the setup for blast changed, in the following entries is a >> non-terminating blast call. They do not seam to be related to the change >> at all: >> >> Graph_Theory > > I replaced this 'by

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

Am Sonntag, den 15.11.2015, 11:43 +0100 schrieb Andreas Lochbihler: > Vickey_Clarke_Groves looks related to the changes to "real", but I > have not tried to fix this. This should be fixed now in AFP e6d87060e398. - Johannes ___ isabelle-dev mailing