src/Tools/Profiling.thy
author wenzelm
Wed, 29 May 2024 16:06:07 +0200
changeset 80211 2ec1b11f1f93
parent 78315 addecc8de2c4
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
     1
(*  Title:      Tools/profiling.ML
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
     2
    Author:     Makarius
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     3
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
     4
Session profiling based on loaded ML image.
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     5
*)
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     6
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
     7
theory Profiling
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     8
  imports Pure
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
     9
begin
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    10
78315
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    11
ML_file "profiling.ML"
addecc8de2c4 proper system integration and renaming;
wenzelm
parents: 78314
diff changeset
    12
ML_command \<open>Profiling.main ()\<close>
78314
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    13
1588bec693c2 copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff changeset
    14
end