[isabelle-dev] the function "real"

[Lars Noschinski]

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 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.