# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 8488fdc4ddc0062c5fe3cb94222c3f8f5e9b11a3
# Parent  8ae6f86a347726854f723f586103d16b48c77c18
minimized Nitpick's dependencies

diff -r 8ae6f86a3477 -r 8488fdc4ddc0 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -12,7 +12,7 @@
    suite. *)
 
 theory Manual_Nits
-imports Main Real "~~/src/HOL/Library/Quotient_Product" "~~/src/HOL/BNF/BNF"
+imports Main Real "~~/src/HOL/Library/Quotient_Product"
 begin
 
 chapter {* 2. First Steps *}
diff -r 8ae6f86a3477 -r 8488fdc4ddc0 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/ROOT	Mon Jan 20 18:24:56 2014 +0100
@@ -240,7 +240,7 @@
     Trans_Closure
     Sets
 
-session "HOL-BNF-Nitpick_Examples" in Nitpick_Examples = "HOL-BNF" +
+session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
   description {*
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009