isabelle: src/Pure/ML-Systems/polyml-5.0.ML@a010aab5bed0 (annotated)

21653 219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	1	(* Title: Pure/ML-Systems/polyml-5.0.ML
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	2
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	3	Compatibility wrapper for Poly/ML 5.0.
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	4	*)
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	5
28151 61f9c918b410 explicit use of universal.ML and dummy_thread.ML; wenzelm parents: 26378 diff changeset	6	use "ML-Systems/universal.ML";
61f9c918b410 explicit use of universal.ML and dummy_thread.ML; wenzelm parents: 26378 diff changeset	7	use "ML-Systems/thread_dummy.ML";
26215 94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x; wenzelm parents: 24605 diff changeset	8	use "ML-Systems/polyml_common.ML";
26378 bac8d5e5f833 moved use_text/file to polyml_old_compiler5.ML; wenzelm parents: 26215 diff changeset	9	use "ML-Systems/polyml_old_compiler5.ML";
21653 219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	10
219924615db6 setup for polyml-5.0; wenzelm parents: diff changeset	11	val pointer_eq = PolyML.pointerEq;
21771 148c8aba89dd added improved versions of use_text/file (still inactive); wenzelm parents: 21653 diff changeset	12