HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned
authorhoelzl
Thu, 18 Aug 2016 11:00:36 +0200
changeset 63716 91a0494d8a4a
parent 63715 ad2c003782f9
child 63717 3b0500bd2240
HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned
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