[isabelle-dev] NEWS: method facts

[Joachim Breitner]

Hi,

Am Mittwoch, den 08.06.2016, 19:46 +0200 schrieb Makarius:
> There are further possibilities for "use", e.g. to eliminate
> auxiliary
> "-" or "insert" steps, notably:
> 
>   qed (insert a, auto)  ~>  qed (use a in auto)

does this mean that the old idiom of

    lemma foo:
      assumes "inductive_predicate x"
      shows "something_about x"
    using assms
    proof(induction x)
     ...
    qed

can (and should) now become the slightly nicer

    lemma foo:
      assumes "inductive_predicate x"
      shows "something_about x"
    p
    roof(use assms in ‹induction x›)
     ...
    qed

or is the need for method nesting no better than the extra using assms?


Thanks,
Joachim

-- 
Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160609/62b25e9c/attachment.sig>