--- a/PrioG.thy	Fri Dec 18 22:47:32 2015 +0800
+++ b/PrioG.thy	Tue Dec 22 23:13:31 2015 +0800
@@ -2923,6 +2923,5 @@
   shows "th1 = th2"
 using assms by (unfold next_th_def, auto)
 
-
  
 end