[isabelle-dev] the function "real"

[Tobias Nipkow]

On 12/11/2015 13:03, Lawrence Paulson wrote:
> I’m going to try to make the other change as well. The problem is that for a great many theorems, their behaviour with the simplifier and/or blast differed according to which coercion function they were expressed with. This makes it impossible to duplicate the prior behaviour. I have already observed that adding these additional simplification rules breaks a few proofs, so we have to see how it goes.

I am not surprised at all that the simplifier behaves differently because the 
simpset is modified all the time and is full of theorems wih coercions. But 
blast is another matter. Concrete questions:

- Are there any coercion-related permanent intro/dest/elim theorems (either 
before or now)?

- Could they kick in during a proof concerned only with basic set theory and 
first order logic?

I want to make sure that it is not something else that caused blast to break.

Tobias

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151112/de07996c/attachment.bin>