changeset 62 | 031d2ae9c9b8 |
parent 61 | f8194fd6214f |
child 63 | b620a2a0806a |
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 |