2016-02-03 updated files
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 03 Feb 2016 14:37:35 +0000] rev 106
updated files
2016-02-03 Commit to revert
zhangx [Wed, 03 Feb 2016 22:17:29 +0800] rev 105
Commit to revert
2016-02-03 A fake merge. Used to revert to 98
zhangx [Wed, 03 Feb 2016 21:51:57 +0800] rev 104
A fake merge. Used to revert to 98
2016-02-03 PIPBasics.thy reorganized into sections. The structure is now stable. Next step is to put in more comments.
zhangx [Wed, 03 Feb 2016 21:41:42 +0800] rev 103
PIPBasics.thy reorganized into sections. The structure is now stable. Next step is to put in more comments.
2016-02-03 Reorganizing PIPBasics.thy and making small changes to Implementation.thy and Correctness.thy.
zhangx [Wed, 03 Feb 2016 21:05:15 +0800] rev 102
Reorganizing PIPBasics.thy and making small changes to Implementation.thy and Correctness.thy.
2016-02-03 Reorganzing PIPBasics.thy intro sections.
zhangx [Wed, 03 Feb 2016 12:04:03 +0800] rev 101
Reorganzing PIPBasics.thy intro sections.
2016-02-01 Reorganizing PIPBasics.thy
zhangx [Mon, 01 Feb 2016 20:56:39 +0800] rev 100
Reorganizing PIPBasics.thy
2016-01-31 Small improvemnts in PIPBasis.thy
zhangx [Sun, 31 Jan 2016 18:15:13 +0800] rev 99
Small improvemnts in PIPBasis.thy
2016-01-29 deleted superflous files
Christian Urban <christian dot urban at kcl dot ac dot uk> [Fri, 29 Jan 2016 17:08:54 +0000] rev 98
deleted superflous files
2016-01-29 merged
Christian Urban <christian dot urban at kcl dot ac dot uk> [Fri, 29 Jan 2016 17:06:02 +0000] rev 97
merged
2016-01-28 merged
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 28 Jan 2016 14:57:36 +0000] rev 96
merged
2016-01-28 changes to my repository
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 28 Jan 2016 14:26:10 +0000] rev 95
changes to my repository
2016-01-28 some small changes
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 28 Jan 2016 13:46:45 +0000] rev 94
some small changes
2016-01-29 The overwriten original .thy files are working now. The ones in last revision aren't.
zhangx [Fri, 29 Jan 2016 11:01:13 +0800] rev 93
The overwriten original .thy files are working now. The ones in last revision aren't.
2016-01-29 Original files overwrite by their parallels (Correctness.thy v.s. PrioG.thy, PIPBasics.thy v.s. CpsG.thy, Implementation v.s. ExtGG.thy).
zhangx [Fri, 29 Jan 2016 10:51:52 +0800] rev 92
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 Removed *.*~, #***#, log, etc.
zhangx [Fri, 29 Jan 2016 09:46:07 +0800] rev 91
Removed *.*~, #***#, log, etc.
2016-01-28 Retrofiting of:
zhangx [Thu, 28 Jan 2016 21:14:17 +0800] rev 90
Retrofiting of: CpsG.thy (the parallel copy of PIPBasics.thy), ExtGG.thy (The paralell copy of Implemenation.thy), PrioG.thy (The paralell copy of Correctness.thy) has completed. The next step is to overwite original copies with the paralell ones.
2016-01-28 Slightly modified ExtGG.thy and PrioG.thy.
zhangx [Thu, 28 Jan 2016 16:36:46 +0800] rev 89
Slightly modified ExtGG.thy and PrioG.thy.
2016-01-28 Merged back ExtGG.thy and PrioG.thy.
zhangx [Thu, 28 Jan 2016 16:33:49 +0800] rev 88
Merged back ExtGG.thy and PrioG.thy.
2016-01-28 Tracking ExtGG.thy etc., so that a update to 83 is possible.
zhangx [Thu, 28 Jan 2016 15:36:48 +0800] rev 87
Tracking ExtGG.thy etc., so that a update to 83 is possible.
2016-01-27 Added PrioG.thy again
zhangx [Thu, 28 Jan 2016 07:46:05 +0800] rev 86
Added PrioG.thy again
2016-01-27 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx [Thu, 28 Jan 2016 07:43:05 +0800] rev 85
Added PrioG.thy as a parallel copy of Correctness.thy
2016-01-27 The parallel of Implementation.thy, i.e. ExtGG.thy has been updated. And some errors in
zhangx [Wed, 27 Jan 2016 23:34:23 +0800] rev 84
The parallel of Implementation.thy, i.e. ExtGG.thy has been updated. And some errors in CpsG.thy have also been corrected.
2016-01-27 merged
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 27 Jan 2016 13:50:02 +0000] rev 83
merged
2016-01-27 some small changes to Correctness and Paper
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 27 Jan 2016 13:47:08 +0000] rev 82
some small changes to Correctness and Paper
2016-01-27 CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
zhangx [Wed, 27 Jan 2016 19:28:42 +0800] rev 81
CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
2016-01-27 CpsG.thy retrofiting almost completed. An important mile stone.
zhangx [Wed, 27 Jan 2016 19:26:56 +0800] rev 80
CpsG.thy retrofiting almost completed. An important mile stone.
2016-01-17 Still improving CpsG.thy
zhangx [Sun, 17 Jan 2016 22:18:35 +0800] rev 79
Still improving CpsG.thy
2016-01-16 Merged with 77
zhangx [Sat, 16 Jan 2016 11:02:17 +0800] rev 78
Merged with 77
2016-01-16 CpsG.thy updated. It is a copy of PIPBasics.thy under drastic improvement.
zhangx [Sat, 16 Jan 2016 10:59:03 +0800] rev 77
CpsG.thy updated. It is a copy of PIPBasics.thy under drastic improvement.
2016-01-15 some small changes to the paper
Christian Urban <christian dot urban at kcl dot ac dot uk> [Fri, 15 Jan 2016 02:05:29 +0000] rev 76
some small changes to the paper
2016-01-14 updated paper
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 14 Jan 2016 03:29:22 +0000] rev 75
updated paper
2016-01-13 Moment.thy further simplified.
zhangx [Thu, 14 Jan 2016 00:55:54 +0800] rev 74
Moment.thy further simplified.
2016-01-13 Moment.thy further improved.
zhangx [Wed, 13 Jan 2016 23:39:59 +0800] rev 73
Moment.thy further improved.
2016-01-13 another simplification
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 13 Jan 2016 15:22:14 +0000] rev 72
another simplification
2016-01-13 some small change
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 13 Jan 2016 15:16:59 +0000] rev 71
some small change
2016-01-13 further simplificaton of Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 13 Jan 2016 14:20:58 +0000] rev 70
further simplificaton of Moment.thy
2016-01-13 simplified Moment.thy
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 13 Jan 2016 13:20:45 +0000] rev 69
simplified Moment.thy
2016-01-12 Before retrofiting PIPBasics.thy
zhangx [Tue, 12 Jan 2016 08:35:36 +0800] rev 68
Before retrofiting PIPBasics.thy
2016-01-09 Correctness simplified a great deal.
zhangx [Sat, 09 Jan 2016 22:19:27 +0800] rev 67
Correctness simplified a great deal.
2016-01-07 Some small improvements in Correctness.thy.
zhangx [Thu, 07 Jan 2016 22:10:06 +0800] rev 66
Some small improvements in Correctness.thy.
2016-01-07 Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx [Thu, 07 Jan 2016 08:33:13 +0800] rev 65
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
2016-01-06 renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 06 Jan 2016 16:34:26 +0000] rev 64
renamed files
2016-01-06 ExtGG.thy finished, but more comments are needed.
zhangx [Wed, 06 Jan 2016 20:46:14 +0800] rev 63
ExtGG.thy finished, but more comments are needed.
2015-12-22 In the middle of retrofiting ExtGG.thy.
zhangx [Tue, 22 Dec 2015 23:13:31 +0800] rev 62
In the middle of retrofiting ExtGG.thy.
2015-12-18 CpsG.thy has been cleaned up.
zhangx [Fri, 18 Dec 2015 22:47:32 +0800] rev 61
CpsG.thy has been cleaned up. The next step is to add more comments and make slight changes along the way.
2015-12-18 Main proofs in CpsG.thy completed.
zhangx [Fri, 18 Dec 2015 19:13:19 +0800] rev 60
Main proofs in CpsG.thy completed. The next step is to remove lemmas unused in new proofs.
2015-12-15 removed some fixes about which Isabelle complains
Christian Urban <christian dot urban at kcl dot ac dot uk> [Tue, 15 Dec 2015 15:10:40 +0000] rev 59
removed some fixes about which Isabelle complains
2015-12-15 Extended RTree.thy
zhangx [Tue, 15 Dec 2015 21:45:46 +0800] rev 58
Extended RTree.thy
2015-12-03 Added generic theory "RTree.thy"
xingyuan zhang <xingyuanzhang@126.com> [Thu, 03 Dec 2015 14:34:29 +0800] rev 57
Added generic theory "RTree.thy"
2015-12-03 Before switching to generic theory of relational trees.
xingyuan zhang <xingyuanzhang@126.com> [Thu, 03 Dec 2015 14:34:00 +0800] rev 56
Before switching to generic theory of relational trees.
2015-10-30 Comments for Set-operation finished
xingyuan zhang <xingyuanzhang@126.com> [Fri, 30 Oct 2015 20:40:11 +0800] rev 55
Comments for Set-operation finished
2015-10-17 Merge with tip
xingyuan zhang <xingyuanzhang@126.com> [Sat, 17 Oct 2015 16:14:30 +0800] rev 54
Merge with tip
2015-10-17 Finished comments on PrioGDef.thy
xingyuan zhang <xingyuanzhang@126.com> [Sat, 17 Oct 2015 16:10:33 +0800] rev 53
Finished comments on PrioGDef.thy
2015-10-06 test
Christian Urban <christian dot urban at kcl dot ac dot uk> [Tue, 06 Oct 2015 14:22:34 +0100] rev 52
test
2015-10-06 another test
Christian Urban <christian dot urban at kcl dot ac dot uk> [Tue, 06 Oct 2015 14:13:52 +0100] rev 51
another test
2015-10-06 test
Christian Urban <christian dot urban at kcl dot ac dot uk> [Tue, 06 Oct 2015 14:11:28 +0100] rev 50
test
2015-10-06 A little more change.
xingyuan zhang <xingyuanzhang@126.com> [Tue, 06 Oct 2015 18:52:04 +0800] rev 49
A little more change.
2015-10-06 Some changes in the PrioGDef.thy.
xingyuan zhang <xingyuanzhang@126.com> [Tue, 06 Oct 2015 13:08:00 +0800] rev 48
Some changes in the PrioGDef.thy.
2015-10-06 Just a test change
xingyuan zhang <xingyuanzhang@126.com> [Tue, 06 Oct 2015 11:26:18 +0800] rev 47
Just a test change
(0) -100 -60 +60 +100 tip