# HG changeset patch
# User paulson
# Date 975947440 -3600
# Node ID 1db42f739ee72a1e68c1f84bf0f2424a0ef7cae4
# Parent  b325139714819781415582fe32b00f5d4e85a878
loads the new theory Numbers.thy

diff -r b32513971481 -r 1db42f739ee7 doc-src/TutorialI/Types/ROOT.ML
--- a/doc-src/TutorialI/Types/ROOT.ML	Mon Dec 04 17:30:15 2000 +0100
+++ b/doc-src/TutorialI/Types/ROOT.ML	Mon Dec 04 17:30:40 2000 +0100
@@ -1,4 +1,6 @@
+(* ID:         $Id$ *)
 use "../settings.ML";
+use_thy "Numbers";
 use_thy "Pairs";
 use_thy "Typedef";
 use_thy "Overloading0";