| changeset 16470 | 051db5bb21b5 |
| parent 16469 | 7e27422c603e |
| child 16502 | 5a56e59526a5 |
--- 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 **)