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
signature.asc
Description: This is a digitally signed message part
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
