[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
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 archive was generated by a fusion of
Pipermail (Mailman edition) and