author | wenzelm |
Sun, 19 Jun 2005 00:07:41 +0200 | |
changeset 16470 | 051db5bb21b5 |
parent 16469 | 7e27422c603e |
child 16471 | c487e7e8865f |
--- a/src/Pure/ML-Systems/mosml.ML Sun Jun 19 00:02:06 2005 +0200 +++ b/src/Pure/ML-Systems/mosml.ML Sun Jun 19 00:07:41 2005 +0200 @@ -12,6 +12,9 @@ > val ml_system = "mosml"; > use "ML-Systems/mosml.ML"; > use "ROOT.ML"; +> Session.finish (); +> cd "../HOL"; +> use "ROOT.ML"; *) (** ML system related **)