added Real to BasisLibrary
authorpaulson
Fri Oct 02 10:44:20 1998 +0200 (1998-10-02)
changeset 56075db9e2343ade
parent 5606 39d68cfa457d
child 5608 a82a038a3e7a
added Real to BasisLibrary
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Fri Oct 02 10:43:08 1998 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Oct 02 10:44:20 1998 +0200
     1.3 @@ -65,7 +65,9 @@
     1.4  struct
     1.5    structure List   = List 
     1.6    and       Option = Option
     1.7 -  and       Int    = Int;
     1.8 +  and       Bool   = Bool
     1.9 +  and       Int    = Int
    1.10 +  and       Real   = Real;
    1.11  end;
    1.12  
    1.13  open Use;