blanchet@33197: (* Title: HOL/Nitpick_Examples/Nitpick_Examples.thy blanchet@33197: Author: Jasmin Blanchette, TU Muenchen blanchet@45035: Copyright 2009-2011 blanchet@33197: blanchet@33197: Nitpick examples. blanchet@33197: *) blanchet@33197: blanchet@33197: theory Nitpick_Examples blanchet@35076: imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits blanchet@45035: Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits blanchet@45035: Tests_Nits Typedef_Nits blanchet@33197: begin blanchet@33197: end