[isabelle-dev] the function "real"
noschinl at in.tum.de
Thu Nov 12 13:58:47 CET 2015
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.
More information about the isabelle-dev