src/Pure/ML/ml_statistics_dummy.ML
author wenzelm
Wed, 30 Dec 2015 21:57:52 +0100
changeset 62002 f1599e98c4d0
parent 50280 0eb9b5d09f31
permissions -rw-r--r--
isabelle update_cartouches -c -t;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_statistics_dummy.ML
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     3
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     4
ML runtime statistics -- dummy version.
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     5
*)
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     6
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     7
signature ML_STATISTICS =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     8
sig
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
     9
  val get: unit -> Properties.T
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    10
end;
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    11
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    12
structure ML_Statistics: ML_STATISTICS =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    13
struct
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    14
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    15
fun get () = [];
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    16
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    17
end;
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents:
diff changeset
    18