src/Tools/Metis/metis_env.ML
changeset 23452 95b70054bb3a
child 33004 715566791eb0
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/metis_env.ML	Thu Jun 21 13:53:53 2007 +0200
@@ -0,0 +1,5 @@
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;