isabelle: src/Pure/RAW/ROOT_polyml-5.6.ML@d3996d5873dd (annotated)

62077 e8ae72c26025 clarified ROOT files; wenzelm parents: 61925 diff changeset	1	(* Title: Pure/RAW/ROOT_polyml-5.6.ML
61715 5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	2	Author: Makarius
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	3
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	4	Compatibility wrapper for Poly/ML 5.6.
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	5	*)
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	6
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	7	structure Thread =
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	8	struct
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	9	open Thread;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	10
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	11	structure Thread =
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	12	struct
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	13	open Thread;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	14
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	15	fun numProcessors () =
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	16	(case Thread.numPhysicalProcessors () of
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	17	SOME n => n
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	18	\| NONE => Thread.numProcessors ());
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	19	end;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	20	end;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	21
62077 e8ae72c26025 clarified ROOT files; wenzelm parents: 61925 diff changeset	22	use "RAW/ROOT_polyml.ML";

author	wenzelm
	Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337	d3996d5873dd
parent 62077	e8ae72c26025
permissions	-rw-r--r--