--- a/CpsG.thy	Sat Feb 06 23:42:03 2016 +0800
+++ b/CpsG.thy	Sun Feb 07 21:21:53 2016 +0800
@@ -4657,6 +4657,13 @@
   using vt assms next_th_holding next_th_waiting
   by (unfold s_RAG_def, simp)
 
+end 
+
+context valid_trace_p
+begin
+
+find_theorems readys th
+
 end
 
 end
\ No newline at end of file