src/HOL/Nitpick_Examples/ROOT.ML
author blanchet
Thu, 16 Sep 2010 16:12:02 +0200
changeset 39494 bf7dd4902321
parent 37495 650fae5eea93
child 39616 8052101883c3
permissions -rw-r--r--
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"

(*  Title:      HOL/Nitpick_Examples/ROOT.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009

Nitpick examples.
*)

setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"];