[isabelle-dev] smt2

[Makarius]

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