makarius at sketis.net
Fri Mar 14 16:14:43 CET 2014
On Fri, 14 Mar 2014, Andreas Lochbihler wrote:
> To make one's type work with narrowing, however, is hardly documented.
> Recently, I finally got around to provide narrowing generators for
> Coinductive in the AFP (AFP/1fffd2ebbd28), but I had to study all the
> implementation of the narrowing engine and read up on SmallCheck in
> order to understand just how to do it. We definitely cannot expect most
> users to figure this out themselves.
How about writing one or two paragraphs for the isar-ref manual, and get
added to the list of its contributors?
(This is independent of the question of main HOL vs. HOL-Library.)
More information about the isabelle-dev