--- a/Test.thy	Tue Jul 15 17:25:53 2014 +0200
+++ b/Test.thy	Wed Sep 09 11:24:19 2015 +0100
@@ -749,10 +749,6 @@
 
 
 
-
-done
-
-
   (*
   obtain th0 where th0_in: "th0 \<in> S1 \<and> th0 \<in> S2" 
     and eq_f_th0: "preced th0 s = Max ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"
@@ -784,4 +780,6 @@
   qed
   *)
 
+thm waits_def waits2_def
+
 end
\ No newline at end of file