Good idea. Please ensure that some of them are brand-new users. Larry On 5 Sep 2012, at 14:46, Makarius <makarius at sketis.net> wrote: > What I need is to watch over the shoulders of more people trying to write Isar proofs in the current Prover IDE. In May this year I had 15 people and 2 days to get some impressions where to continue next.