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



Dear Isabelle Gurus,

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?

Sincerely,

Rafal Kolanski.






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