src/HOL/Nitpick_Examples/Nitpick_Examples.thy
author wenzelm
Thu, 03 Sep 2015 19:27:45 +0200
changeset 61109 1c98bfc5d743
parent 45035 60d2c03d5c70
permissions -rw-r--r--
proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";

(*  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