# HG changeset patch
# User nipkow
# Date 1149863105 -7200
# Node ID 1a09f25410da0681c2ede6c08da754fb30c8f0cd
# Parent  c00e04f8a52a6098b0eb7d2f21050ae78134ee77
nbe -> NormalForm

diff -r c00e04f8a52a -r 1a09f25410da src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Jun 09 14:20:09 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Jun 09 16:25:05 2006 +0200
@@ -60,7 +60,7 @@
 
 time_use_thy "Refute_Examples";
 time_use_thy "Quickcheck_Examples";
-no_document time_use_thy "nbe";
+no_document time_use_thy "NormalForm";
 
 no_document use_thy "Word";
 time_use_thy "Adder";