src/Pure/RAW/polyml-5.6.ML
author wenzelm
Sat, 26 Dec 2015 15:03:41 +0100
changeset 61931 ed47044ee6a6
parent 61925 ab52f183f020
permissions -rw-r--r--
more proofs, more text;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 61715
diff changeset
     1
(*  Title:      Pure/RAW/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
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 61715
diff changeset
    22
use "RAW/polyml.ML";