* New testing tool "Mirabelle" for automated (proof) tools. Applies several tools and tactics like sledgehammer, metis, or quickcheck, to every proof step in a theory. To be used in batch mode via "isabelle mirabelle".