# HG changeset patch
# User paulson
# Date 907317860 -7200
# Node ID 5db9e2343ade30fa93233e32a9c7ee5e4db2ce21
# Parent  39d68cfa457de5d816f78e8c13ec34e7ecbe52d7
added Real to BasisLibrary

diff -r 39d68cfa457d -r 5db9e2343ade src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Oct 02 10:43:08 1998 +0200
+++ b/src/Pure/ROOT.ML	Fri Oct 02 10:44:20 1998 +0200
@@ -65,7 +65,9 @@
 struct
   structure List   = List 
   and       Option = Option
-  and       Int    = Int;
+  and       Bool   = Bool
+  and       Int    = Int
+  and       Real   = Real;
 end;
 
 open Use;