Re: [isabelle] Preferred citation for the induct(ion) method and the induct_tac method.
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Preferred citation for the induct(ion) method and the induct_tac method.
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Tue, 1 Oct 2019 11:59:27 +0200
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:68.0) Gecko/20100101 Thunderbird/68.1.1
The first part of the book Concrete Semantics contains an intro to Isabelle that
also covers induction.
On 30/09/2019 10:19, Nagashima, Yutaka wrote:
Is there any paper I should cite when discussing these proof methods?
I used to cite only the old tutorial of Isabelle/HOL when writing about automating induction in Isabelle/HOL.
But maybe this was wrong, and I should cite some papers about these method.
Description: S/MIME Cryptographic Signature
This archive was generated by a fusion of
Pipermail (Mailman edition) and