src/HOL/Nitpick_Examples/ROOT.ML
author blanchet
Tue, 07 Dec 2010 11:56:01 +0100
changeset 41045 2a41709f34c1
parent 39616 8052101883c3
permissions -rw-r--r--
use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets

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

Nitpick examples.
*)

Unsynchronized.setmp quick_and_dirty true use_thys ["Nitpick_Examples"];