src/Pure/ML-Systems/polyml-5.0.ML
changeset 29564 f8b933a62151
parent 28151 61f9c918b410
child 29638 1f8f3d26a2cf
equal deleted inserted replaced
29563:4773c5c994dc 29564:f8b933a62151
     1 (*  Title:      Pure/ML-Systems/polyml-5.0.ML
     1 (*  Title:      Pure/ML-Systems/polyml-5.0.ML
     2     ID:         $Id$
       
     3 
     2 
     4 Compatibility wrapper for Poly/ML 5.0.
     3 Compatibility wrapper for Poly/ML 5.0.
     5 *)
     4 *)
     6 
     5 
     7 use "ML-Systems/universal.ML";
     6 use "ML-Systems/universal.ML";