src/Pure/ML-Systems/polyml_common.ML
2008-03-28 wenzelm 2008-03-28 added forget_structure;
2008-03-24 wenzelm 2008-03-24 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1); moved use_text/file to polyml_old_compiler4.ML; PolyML.onEntry: no longer evaluate command line;
2008-03-06 wenzelm 2008-03-06 common setup for system_out/system;
2008-03-06 wenzelm 2008-03-06 rearrangements to make latest Poly/ML the default, not old 4.x;