# HG changeset patch
# User wenzelm
# Date 1509570818 -3600
# Node ID 5188b1c5943434912b017b91b43b14828ae13cdb
# Parent  7382ff5b46b931e899afd57d55efe174c7506dcc
more timing;

diff -r 7382ff5b46b9 -r 5188b1c59434 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Nov 01 21:21:09 2017 +0100
+++ b/src/HOL/ROOT	Wed Nov 01 22:13:38 2017 +0100
@@ -371,7 +371,7 @@
     Games
   document_files "root.tex"
 
-session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
+session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
   options [print_mode = "iff,no_brackets"]
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"