[isabelle-dev] the function "real"
noschinl at in.tum.de
Mon Nov 16 14:05:48 CET 2015
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:
> I replaced this 'by safe meson+' now. I am a bit surprised that this
> proof broke, it is just basic set theory and first order logic.
Ok, bisected to the change which broke this proof: it is 933eb9e6a1cc by
Larry. The good news is the current head unbroke the proof agian.
More information about the isabelle-dev