# HG changeset patch
# User haftmann
# Date 1451232511 -3600
# Node ID 844881193616ed5ed490bcdc4e5db3e4a3fcfc26
# Parent  1135b8de26c3b3e050428aec1266371a1f27e7f4
put example into separate session, to restrict precious session image to library theories

diff -r 1135b8de26c3 -r 844881193616 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Dec 28 01:28:28 2015 +0100
+++ b/src/HOL/ROOT	Sun Dec 27 17:08:31 2015 +0100
@@ -735,11 +735,14 @@
     "~~/src/HOL/Library/Diagonal_Subsequence"
   theories
     Probability
-    "ex/Dining_Cryptographers"
-    "ex/Koepf_Duermuth_Countermeasure"
-    "ex/Measure_Not_CCC"
   document_files "root.tex"
 
+session "HOL-Probability-ex" in "Probability/ex" = "HOL-Probability" +
+  theories
+    "Dining_Cryptographers"
+    "Koepf_Duermuth_Countermeasure"
+    "Measure_Not_CCC"
+
 session "HOL-Nominal" in Nominal = HOL +
   options [document = false]
   theories Nominal