# HG changeset patch
# User wenzelm
# Date 1142092390 -3600
# Node ID 613f374ea27df09e2c1a013ebd5b2d25fb8014a2
# Parent  3a73cb17a707827f1919ac1c6603b6a08d710cfe
nbe: no_document;

diff -r 3a73cb17a707 -r 613f374ea27d src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Mar 10 19:49:58 2006 +0100
+++ b/src/HOL/ex/ROOT.ML	Sat Mar 11 16:53:10 2006 +0100
@@ -57,7 +57,7 @@
 
 time_use_thy "Refute_Examples";
 time_use_thy "Quickcheck_Examples";
-time_use_thy "nbe";
+no_document time_use_thy "nbe";
 
 no_document use_thy "Word";
 time_use_thy "Adder";