Re: [isabelle-dev] Testing AFP at TUM [was: Isabelle cs. 70300f1b6835]

2012-10-22 Thread Makarius
On Mon, 22 Oct 2012, Gerwin Klein wrote: On 22/10/2012, at 1:46 AM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Yes, I know. I already fixed Collections on Friday and I am going to go back to this problem on Monday. Btw. whenever I'm testing the AFP these days

Re: [isabelle-dev] Testing AFP at TUM

2012-10-22 Thread Tjark Weber
On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote: Btw. whenever I'm testing the AFP these days without relying on the testboard I use the following [...] In the last few months I've seen several emails with testing advice on this list (occasionally motivated by commits that apparently

Re: [isabelle-dev] Testing AFP at TUM

2012-10-22 Thread Makarius
On Mon, 22 Oct 2012, Tjark Weber wrote: On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote: Btw. whenever I'm testing the AFP these days without relying on the testboard I use the following [...] In the last few months I've seen several emails with testing advice on this list

Re: [isabelle-dev] Testing AFP at TUM

2012-10-22 Thread Tobias Nipkow
Am 22/10/2012 14:16, schrieb Tjark Weber: On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote: Btw. whenever I'm testing the AFP these days without relying on the testboard I use the following [...] In the last few months I've seen several emails with testing advice on this list

Re: [isabelle-dev] Testing AFP at TUM

2012-10-22 Thread Makarius
On Mon, 22 Oct 2012, Makarius wrote: Apart from that we have a split into old-school manual testing (what used to be makeall all and is now build -a as shown in the System manual, vs. newer mira/testboard. In Isabelle/8b50286c36d3 it is section 3.3 of the system manual, subsection Examples.