# HG changeset patch
# User paulson
# Date 914860067 -3600
# Node ID dfdb7584cf9676f151eff928b17ca6f988832a11
# Parent  b0895662fba467c73a7406a9cc8ca0462ea96721
String added to BasisLibrary

diff -r b0895662fba4 -r dfdb7584cf96 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Dec 28 16:47:21 1998 +0100
+++ b/src/Pure/ROOT.ML	Mon Dec 28 16:47:47 1998 +0100
@@ -64,7 +64,7 @@
 
 use "install_pp.ML";
 
-(*if true then some packages won't be too serious about actually proving things*)
+(*if true then some packages will OMIT SOME PROOFS*)
 val quick_and_dirty = ref false;
 
 (*several object-logics declare theories that hide basis library structures*)
@@ -73,6 +73,7 @@
   structure List   = List 
   and       Option = Option
   and       Bool   = Bool
+  and       String = String
   and       Int    = Int
   and       Real   = Real;
 end;