# HG changeset patch
# User hoelzl
# Date 1471510836 -7200
# Node ID 91a0494d8a4a0fb9d95df1572e4f1d267548b048
# Parent  ad2c003782f9c977477b649711a715c87619ff91
HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned

diff -r ad2c003782f9 -r 91a0494d8a4a src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Thu Aug 18 13:12:53 2016 +0200
+++ b/src/HOL/Probability/Probability.thy	Thu Aug 18 11:00:36 2016 +0200
@@ -4,12 +4,13 @@
 
 theory Probability
 imports
+  Central_Limit_Theorem
   Discrete_Topology
-  SPMF
   PMF_Impl
-  Stream_Space
+  Projective_Limit
   Random_Permutations
-  Central_Limit_Theorem
+  SPMF
+  Stream_Space
 begin
 
 end