Dear Markarius, Am Donnerstag, den 09.06.2016, 15:58 +0200 schrieb Makarius: > > [..] Turning 'using' into "use" is a downgrade of proof command into proof > method. This is occasionally useful, like e.g. using attribute > expressions instead of proof methods, but not something I would do all > the time. > > First-class tickets on the Isar train are preferable.
thanks for that view on things, and the stratificationof the lange makes sense. But while I like "using" inside an proof, it does not please my sense of aesthetic to have such a command before the initial "proof" command. Maybe a way out would be to take inspiration of how we can avoid some explicit fact chaining inside proof..qed blocks, namely using "thus" instead of "then show", and apply the usual logic of “appending s moves a command from the local variant to the corresponding context specification command”. This would allow me to write (applying the usual rules of the English grammer): lemma foo: assumes "inductive_predicate x" thuses "something_about x" proof(use assms in ‹induction x›) ... qed SCNR, 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
