Hi Jasmin, On Wed, 2013-02-13 at 09:09 +0100, Jasmin Christian Blanchette wrote: > Thankfully, there's a much easier solution: > using [[metis_verbose = false]] by (metis ...) > or, at the top-level, > declare [[metis_verbose = false]]
It's always nice to find out that a requested feature already exists. Thanks again! Tjark _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
