Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?

Hi Rafal,

> After porting my development from slightly pre-2009 to 2009-1, I've
> noticed that I need to help isabelle out by using '-' more than I used
> to, for example:
> case (Cons x xs)
>   hence a: "blah"
>     and a': "blah2"
>     and IH: "someIH"
> this used to go away by simp or blast, but now I need to say:
>   by - simp
> or
>   by - blast
> I expect this for "by - assumption" as assumption doesn't chain in the
> assumptions, but I find it a little strange that simp no longer does. As
> this looks intentional, can anyone tell me why this has changed?
> Also, in my proofs when using force and auto, I've found I need to put
> in a lot more '!', especially on dest: and intro: arguments, and nearly
> always when saying "intro: ext". Once again, does anyone remember why
> this might be?

This sounds indeed strange.  Somehow erratic proof failures could always
occur due to changes in default rules (esp. for classical reasoning),
but your description sounds like a "systematic change".  Can you provide
me more explicit proof text=

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.