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.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
