equal
deleted
inserted
replaced
2912 text {* |
2912 text {* |
2913 The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived |
2913 The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived |
2914 from the concise and miniature model of PIP given in PrioGDef.thy. |
2914 from the concise and miniature model of PIP given in PrioGDef.thy. |
2915 *} |
2915 *} |
2916 |
2916 |
|
2917 lemma eq_dependants: "dependants (wq s) = dependants s" |
|
2918 by (simp add: s_dependants_abv wq_def) |
|
2919 |
|
2920 lemma next_th_unique: |
|
2921 assumes nt1: "next_th s th cs th1" |
|
2922 and nt2: "next_th s th cs th2" |
|
2923 shows "th1 = th2" |
|
2924 using assms by (unfold next_th_def, auto) |
|
2925 |
|
2926 |
|
2927 |
2917 end |
2928 end |