added Int to BasisLibrary
authorpaulson
Fri Sep 25 14:06:27 1998 +0200 (1998-09-25)
changeset 55680067dd151d7a
parent 5567 99c6ef61288f
child 5569 8c7e1190e789
added Int to BasisLibrary
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Fri Sep 25 14:06:00 1998 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Sep 25 14:06:27 1998 +0200
     1.3 @@ -60,11 +60,12 @@
     1.4  (*if true then some packages won't be too serious about actually proving things*)
     1.5  val quick_and_dirty = ref false;
     1.6  
     1.7 -(*several object-logics declare theories named List or Option, hiding
     1.8 -  the eponymous basis library structures*)
     1.9 +(*several object-logics declare theories that hide basis library structures*)
    1.10  structure BasisLibrary =
    1.11  struct
    1.12 -  structure List = List and Option = Option;
    1.13 +  structure List   = List 
    1.14 +  and       Option = Option
    1.15 +  and       Int    = Int;
    1.16  end;
    1.17  
    1.18  open Use;