clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;
(* Title: HOL/Nitpick_Examples/Nitpick_Examples.thy
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009-2011
Nitpick examples.
*)
theory Nitpick_Examples
imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
Tests_Nits Typedef_Nits
begin
end