String added to BasisLibrary
authorpaulson
Mon Dec 28 16:47:47 1998 +0100 (1998-12-28)
changeset 6038dfdb7584cf96
parent 6037 b0895662fba4
child 6039 01f67f5f8dd0
String added to BasisLibrary
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Mon Dec 28 16:47:21 1998 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Mon Dec 28 16:47:47 1998 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  use "install_pp.ML";
     1.6  
     1.7 -(*if true then some packages won't be too serious about actually proving things*)
     1.8 +(*if true then some packages will OMIT SOME PROOFS*)
     1.9  val quick_and_dirty = ref false;
    1.10  
    1.11  (*several object-logics declare theories that hide basis library structures*)
    1.12 @@ -73,6 +73,7 @@
    1.13    structure List   = List 
    1.14    and       Option = Option
    1.15    and       Bool   = Bool
    1.16 +  and       String = String
    1.17    and       Int    = Int
    1.18    and       Real   = Real;
    1.19  end;