Am 02.05.2012 um 13:55 schrieb Makarius: > On Thu, 26 Apr 2012, Christian Sternagel wrote: > >> I was just curious what "mirabelle" actually is/does, which I still don't >> know. > > I don't know how (or if) it is tested.
The "HOL-Mirabelle" session ensures that the ML code compiles. This already catches 98% of what can go wrong. The script itself isn't tested, but I use it frequently, almost weekly, and I never had problems with it before. Jasmin _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
