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