src/HOL/Probability/Stopping_Time.thy
changeset 66453 cc19f7ca2ed6
parent 64320 ba194424b895
child 67226 ec32cdaab97b
     1.1 --- a/src/HOL/Probability/Stopping_Time.thy	Fri Aug 18 13:55:05 2017 +0200
     1.2 +++ b/src/HOL/Probability/Stopping_Time.thy	Fri Aug 18 20:47:47 2017 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  section {* Stopping times *}
     1.5  
     1.6  theory Stopping_Time
     1.7 -  imports "../Analysis/Analysis"
     1.8 +  imports "HOL-Analysis.Analysis"
     1.9  begin
    1.10  
    1.11  subsection \<open>Stopping Time\<close>