put example into separate session, to restrict precious session image to library theories

--- 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