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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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