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.
2016-02-04 zhangx Several redundant lemmas removed.
2016-02-04 Christian Urban updated Correctness, Implementation and PIPBasics so that they work with Isabelle 2014 and 2015
2016-02-03 Christian Urban updated files
2016-02-03 zhangx Commit to revert
2016-02-03 zhangx A fake merge. Used to revert to 98
2016-02-03 zhangx PIPBasics.thy reorganized into sections. The structure is now stable. Next step is to put in more comments.
2016-02-03 zhangx Reorganizing PIPBasics.thy and making small changes to Implementation.thy and Correctness.thy.
2016-02-03 zhangx Reorganzing PIPBasics.thy intro sections.
2016-02-01 zhangx Reorganizing PIPBasics.thy
2016-01-31 zhangx Small improvemnts in PIPBasis.thy
2016-01-29 Christian Urban deleted superflous files
2016-01-29 Christian Urban merged
2016-01-28 Christian Urban merged
2016-01-28 Christian Urban changes to my repository
2016-01-28 Christian Urban some small changes
2016-01-29 zhangx The overwriten original .thy files are working now. The ones in last revision aren't.
2016-01-29 zhangx Original files overwrite by their parallels (Correctness.thy v.s. PrioG.thy, PIPBasics.thy v.s. CpsG.thy, Implementation v.s. ExtGG.thy).
2016-01-29 zhangx Removed *.*~, #***#, log, etc.
2016-01-28 zhangx Retrofiting of:
2016-01-28 zhangx Slightly modified ExtGG.thy and PrioG.thy.
2016-01-28 zhangx Merged back ExtGG.thy and PrioG.thy.
2016-01-28 zhangx Tracking ExtGG.thy etc., so that a update to 83 is possible.
2016-01-27 zhangx Added PrioG.thy again
2016-01-27 zhangx Added PrioG.thy as a parallel copy of Correctness.thy
2016-01-27 zhangx The parallel of Implementation.thy, i.e. ExtGG.thy has been updated. And some errors in
2016-01-27 Christian Urban merged
2016-01-27 Christian Urban some small changes to Correctness and Paper
2016-01-27 zhangx CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
2016-01-27 zhangx CpsG.thy retrofiting almost completed. An important mile stone.
2016-01-17 zhangx Still improving CpsG.thy
2016-01-16 zhangx Merged with 77
2016-01-16 zhangx CpsG.thy updated. It is a copy of PIPBasics.thy under drastic improvement.
2016-01-15 Christian Urban some small changes to the paper
2016-01-14 Christian Urban updated paper
2016-01-13 zhangx Moment.thy further simplified.
2016-01-13 zhangx Moment.thy further improved.
2016-01-13 Christian Urban another simplification
2016-01-13 Christian Urban some small change
2016-01-13 Christian Urban further simplificaton of Moment.thy
2016-01-13 Christian Urban simplified Moment.thy
2016-01-12 zhangx Before retrofiting PIPBasics.thy
2016-01-09 zhangx Correctness simplified a great deal.
2016-01-07 zhangx Some small improvements in Correctness.thy.
2016-01-07 zhangx Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
2016-01-06 Christian Urban renamed files
2016-01-06 zhangx ExtGG.thy finished, but more comments are needed.
2015-12-22 zhangx In the middle of retrofiting ExtGG.thy.
2015-12-18 zhangx CpsG.thy has been cleaned up.
2015-12-18 zhangx Main proofs in CpsG.thy completed.
2015-12-15 Christian Urban removed some fixes about which Isabelle complains
2015-12-15 zhangx Extended RTree.thy
2015-12-03 xingyuan zhang Added generic theory "RTree.thy"
2015-12-03 xingyuan zhang Before switching to generic theory of relational trees.
2015-10-30 xingyuan zhang Comments for Set-operation finished
2015-10-17 xingyuan zhang Merge with tip
2015-10-17 xingyuan zhang Finished comments on PrioGDef.thy
2015-10-06 Christian Urban test
2015-10-06 Christian Urban another test
(0) -100 -60 +60 tip