PIPBasics.thy
2016-02-06 zhangx More redundant lemmas are reomved.
2016-02-06 zhangx About to change the proof of waiting_unique_pre and waiting_unqie.
2016-02-05 zhangx wq_in_inv and wq_out_inv are removed, a number of loop holes need to be filled.
less more (0) -10 -3 tip