PrioG.thy
changeset 62 031d2ae9c9b8
parent 61 f8194fd6214f
child 63 b620a2a0806a
equal deleted inserted replaced
61:f8194fd6214f 62:031d2ae9c9b8
  2921   assumes nt1: "next_th s th cs th1"
  2921   assumes nt1: "next_th s th cs th1"
  2922   and nt2: "next_th s th cs th2"
  2922   and nt2: "next_th s th cs th2"
  2923   shows "th1 = th2"
  2923   shows "th1 = th2"
  2924 using assms by (unfold next_th_def, auto)
  2924 using assms by (unfold next_th_def, auto)
  2925 
  2925 
  2926 
       
  2927  
  2926  
  2928 end
  2927 end