diff -r d239aa953315 -r 83dd5345d5d0 log
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/log	Thu Jan 28 16:33:49 2016 +0800
@@ -0,0 +1,447 @@
+修改集:      86:2106021bae53
+标签:        tip
+用户:        zhangx
+日期:        Thu Jan 28 07:46:05 2016 +0800
+摘要:        Added PrioG.thy again
+
+修改集:      85:61a4429e7d4d
+父亲:        84:c0a4e840aefe
+父亲:        33:7f87232d9424
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Jan 27 13:50:02 2016 +0000
+摘要:        merged
+
+修改集:      84:c0a4e840aefe
+父亲:        77:b6ea51cd2e88
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Jan 27 13:47:08 2016 +0000
+摘要:        some small changes to Correctness and Paper
+
+修改集:      83:d239aa953315
+用户:        zhangx
+日期:        Thu Jan 28 07:43:05 2016 +0800
+摘要:        Added PrioG.thy as a parallel copy of Correctness.thy
+
+修改集:      82:cfd644dfc3b4
+用户:        zhangx
+日期:        Wed Jan 27 23:34:23 2016 +0800
+摘要:        The parallel of Implementation.thy, i.e. ExtGG.thy has been updated. And some errors in
+
+修改集:      81:c495eb16beb6
+用户:        zhangx
+日期:        Wed Jan 27 19:28:42 2016 +0800
+摘要:        CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
+
+修改集:      80:17305a85493d
+用户:        zhangx
+日期:        Wed Jan 27 19:26:56 2016 +0800
+摘要:        CpsG.thy retrofiting almost completed. An important mile stone.
+
+修改集:      79:8067efcb43da
+用户:        zhangx
+日期:        Sun Jan 17 22:18:35 2016 +0800
+摘要:        Still improving CpsG.thy
+
+修改集:      78:df0334468335
+父亲:        75:d37703e0c5c4
+父亲:        77:b6ea51cd2e88
+用户:        zhangx
+日期:        Sat Jan 16 11:02:17 2016 +0800
+摘要:        Merged with 77
+
+修改集:      77:b6ea51cd2e88
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Fri Jan 15 02:05:29 2016 +0000
+摘要:        some small changes to the paper
+
+修改集:      76:2aa37de77f31
+父亲:        74:83ba2d8c859a
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Jan 14 03:29:22 2016 +0000
+摘要:        updated paper
+
+修改集:      75:d37703e0c5c4
+用户:        zhangx
+日期:        Sat Jan 16 10:59:03 2016 +0800
+摘要:        CpsG.thy updated. It is a copy of PIPBasics.thy under drastic improvement.
+
+修改集:      74:83ba2d8c859a
+用户:        zhangx
+日期:        Thu Jan 14 00:55:54 2016 +0800
+摘要:        Moment.thy further simplified.
+
+修改集:      73:b0054fb0d1ce
+用户:        zhangx
+日期:        Wed Jan 13 23:39:59 2016 +0800
+摘要:        Moment.thy further improved.
+
+修改集:      72:3fa70b12c117
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Jan 13 15:22:14 2016 +0000
+摘要:        another simplification
+
+修改集:      71:04caf0ccb3ae
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Jan 13 15:16:59 2016 +0000
+摘要:        some small change
+
+修改集:      70:92ca2410b3d9
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Jan 13 14:20:58 2016 +0000
+摘要:        further simplificaton of Moment.thy
+
+修改集:      69:1dc801552dfd
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Jan 13 13:20:45 2016 +0000
+摘要:        simplified Moment.thy
+
+修改集:      68:db196b066b97
+用户:        zhangx
+日期:        Tue Jan 12 08:35:36 2016 +0800
+摘要:        Before retrofiting PIPBasics.thy
+
+修改集:      67:25fd656667a7
+用户:        zhangx
+日期:        Sat Jan 09 22:19:27 2016 +0800
+摘要:        Correctness simplified a great deal.
+
+修改集:      66:2af87bb52fca
+用户:        zhangx
+日期:        Thu Jan 07 22:10:06 2016 +0800
+摘要:        Some small improvements in Correctness.thy.
+
+修改集:      65:633b1fc8631b
+用户:        zhangx
+日期:        Thu Jan 07 08:33:13 2016 +0800
+摘要:        Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
+
+修改集:      64:b4bcd1edbb6d
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Jan 06 16:34:26 2016 +0000
+摘要:        renamed files
+
+修改集:      63:b620a2a0806a
+用户:        zhangx
+日期:        Wed Jan 06 20:46:14 2016 +0800
+摘要:        ExtGG.thy finished, but more comments are needed.
+
+修改集:      62:031d2ae9c9b8
+用户:        zhangx
+日期:        Tue Dec 22 23:13:31 2015 +0800
+摘要:        In the middle of retrofiting ExtGG.thy.
+
+修改集:      61:f8194fd6214f
+用户:        zhangx
+日期:        Fri Dec 18 22:47:32 2015 +0800
+摘要:        CpsG.thy has been cleaned up.
+
+修改集:      60:f98a95f3deae
+用户:        zhangx
+日期:        Fri Dec 18 19:13:19 2015 +0800
+摘要:        Main proofs in CpsG.thy completed.
+
+修改集:      59:0a069a667301
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Dec 15 15:10:40 2015 +0000
+摘要:        removed some fixes about which Isabelle complains
+
+修改集:      58:ad57323fd4d6
+用户:        zhangx
+日期:        Tue Dec 15 21:45:46 2015 +0800
+摘要:        Extended RTree.thy
+
+修改集:      57:f1b39d77db00
+用户:        xingyuan zhang <xingyuanzhang@126.com>
+日期:        Thu Dec 03 14:34:29 2015 +0800
+摘要:        Added generic theory "RTree.thy"
+
+修改集:      56:0fd478e14e87
+用户:        xingyuan zhang <xingyuanzhang@126.com>
+日期:        Thu Dec 03 14:34:00 2015 +0800
+摘要:        Before switching to generic theory of relational trees.
+
+修改集:      55:b85cfbd58f59
+用户:        xingyuan zhang <xingyuanzhang@126.com>
+日期:        Fri Oct 30 20:40:11 2015 +0800
+摘要:        Comments for Set-operation finished
+
+修改集:      54:fee01b2858a2
+父亲:        50:8142e80f5d58
+父亲:        53:78adeef368c1
+用户:        xingyuan zhang <xingyuanzhang@126.com>
+日期:        Sat Oct 17 16:14:30 2015 +0800
+摘要:        Merge with tip
+
+修改集:      53:78adeef368c1
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Oct 06 14:22:34 2015 +0100
+摘要:        test
+
+修改集:      52:d462d449505f
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Oct 06 14:13:52 2015 +0100
+摘要:        another test
+
+修改集:      51:38ad30559775
+父亲:        49:8679d75b1d76
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Oct 06 14:11:28 2015 +0100
+摘要:        test
+
+修改集:      50:8142e80f5d58
+用户:        xingyuan zhang <xingyuanzhang@126.com>
+日期:        Sat Oct 17 16:10:33 2015 +0800
+摘要:        Finished comments on PrioGDef.thy
+
+修改集:      49:8679d75b1d76
+用户:        xingyuan zhang <xingyuanzhang@126.com>
+日期:        Tue Oct 06 18:52:04 2015 +0800
+摘要:        A little more change.
+
+修改集:      48:c0f14399c12f
+用户:        xingyuan zhang <xingyuanzhang@126.com>
+日期:        Tue Oct 06 13:08:00 2015 +0800
+摘要:        Some changes in the PrioGDef.thy.
+
+修改集:      47:2e6c8d530216
+用户:        xingyuan zhang <xingyuanzhang@126.com>
+日期:        Tue Oct 06 11:26:18 2015 +0800
+摘要:        Just a test change
+
+修改集:      46:331137d43625
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Sun Oct 04 23:02:57 2015 +0100
+摘要:        added one more reference to an incorrect specification
+
+修改集:      45:fc83f79009bd
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Sep 09 11:24:19 2015 +0100
+摘要:        updated for Isabelle 2015
+
+修改集:      44:f676a68935a0
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Jul 15 17:25:53 2014 +0200
+摘要:        updated teh theories to newer Isabelle version
+
+修改集:      43:45e1d324c493
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Jun 12 10:14:50 2014 +0100
+摘要:        a few additions
+
+修改集:      42:0069bca6dd51
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Jun 10 10:44:48 2014 +0100
+摘要:        added scheduling book
+
+修改集:      41:66ed924aaa5c
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Mon Jun 09 16:01:28 2014 +0100
+摘要:        added another book that makes the error, some more proofs
+
+修改集:      40:0781a2fc93f1
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Jun 03 15:00:12 2014 +0100
+摘要:        added a library about graphs
+
+修改集:      39:7ea6b019ce24
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Mon Jun 02 14:58:42 2014 +0100
+摘要:        updated
+
+修改集:      38:c89013dca1aa
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Fri May 30 07:56:39 2014 +0100
+摘要:        finished proof of acyclity
+
+修改集:      37:c820ac0f3088
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Sat May 24 12:39:12 2014 +0100
+摘要:        simplified RAG_acyclic proof
+
+修改集:      36:af38526275f8
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Fri May 23 15:19:32 2014 +0100
+摘要:        added a test theory for polishing teh proofs
+
+修改集:      35:92f61f6a0fe7
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu May 22 17:40:39 2014 +0100
+摘要:        added a bit more text to the paper and separated a theory about Max
+
+修改集:      34:313acffe63b6
+父亲:        32:9b9f2117561f
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue May 20 12:49:21 2014 +0100
+摘要:        updated ROOT file
+
+修改集:      33:7f87232d9424
+父亲:        29:408ff78ce28f
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed May 14 11:52:53 2014 +0100
+摘要:        test
+
+修改集:      32:9b9f2117561f
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu May 15 16:02:44 2014 +0100
+摘要:        simplified the cp_rec proof
+
+修改集:      31:e861aff29655
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue May 06 14:36:40 2014 +0100
+摘要:        made some modifications.
+
+修改集:      30:8f026b608378
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Mar 12 10:08:20 2014 +0000
+摘要:        added paper
+
+修改集:      29:408ff78ce28f
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Mar 04 16:47:54 2014 +0000
+摘要:        updated readme
+
+修改集:      28:7fa738a9615a
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Mar 04 16:38:38 2014 +0000
+摘要:        updated
+
+修改集:      27:6b1141c5e24c
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Mar 04 15:49:36 2014 +0000
+摘要:        cleaned up
+
+修改集:      26:da7a6ccfa7a9
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Mar 04 15:30:24 2014 +0000
+摘要:        updated
+
+修改集:      25:a9c0eeb00cc3
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Mar 04 15:27:59 2014 +0000
+摘要:        added two more references
+
+修改集:      24:6f50e6a8c6e0
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Mar 04 09:40:40 2014 +0000
+摘要:        some additions
+
+修改集:      23:24e6884d9258
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Mar 04 08:45:11 2014 +0000
+摘要:        made some small chages
+
+修改集:      22:9f0b78fcc894
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Mon Mar 03 16:22:48 2014 +0000
+摘要:        updated
+
+修改集:      21:55d1591b17f0
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Fri Feb 28 12:49:58 2014 +0000
+摘要:        added llncs to journal
+
+修改集:      20:b56616fd88dd
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Tue Feb 25 20:01:47 2014 +0000
+摘要:        added
+
+修改集:      19:3cc70bd49588
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Jun 20 23:28:26 2013 -0400
+摘要:        added paper
+
+修改集:      18:598409a21f4c
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Jun 20 13:50:01 2013 -0400
+摘要:        added nasa talk
+
+修改集:      17:105715a0a807
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Sat Dec 22 14:50:29 2012 +0000
+摘要:        updated
+
+修改集:      16:9764023f719e
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Sat Dec 22 01:58:45 2012 +0000
+摘要:        added
+
+修改集:      15:9e664c268e25
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Fri Dec 21 23:32:58 2012 +0000
+摘要:        added
+
+修改集:      14:1bf194825a4e
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Fri Dec 21 18:06:00 2012 +0000
+摘要:        more one the implementation
+
+修改集:      13:735e36c64a71
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Fri Dec 21 13:30:14 2012 +0000
+摘要:        added explanation of the code
+
+修改集:      12:85116bc854c0
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Fri Dec 21 00:24:30 2012 +0000
+摘要:        updated
+
+修改集:      11:8e02fb168350
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Dec 20 14:54:06 2012 +0000
+摘要:        added
+
+修改集:      10:242a781135ba
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Dec 20 12:23:44 2012 +0000
+摘要:        added two papers about PIP on multiprocs
+
+修改集:      9:a8e8ec87a933
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Dec 20 10:53:31 2012 +0000
+摘要:        added original Sha paper
+
+修改集:      8:5ba3d79622da
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Dec 19 23:46:36 2012 +0000
+摘要:        added a paragraph about RAGS
+
+修改集:      7:0514be2ad83e
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Wed Dec 19 12:51:06 2012 +0000
+摘要:        started code explanation
+
+修改集:      6:7f2493296c39
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Mon Dec 17 12:34:24 2012 +0000
+摘要:        updated
+
+修改集:      5:0f2d4b78f839
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Mon Dec 10 21:27:22 2012 +0000
+摘要:        updated
+
+修改集:      4:9d667d545e32
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Dec 06 16:30:57 2012 +0000
+摘要:        added
+
+修改集:      3:51019d035a79
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Dec 06 15:49:20 2012 +0000
+摘要:        made everything working
+
+修改集:      2:a04084de4946
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Dec 06 15:12:49 2012 +0000
+摘要:        added
+
+修改集:      1:c4783e4ef43f
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Dec 06 15:11:51 2012 +0000
+摘要:        added
+
+修改集:      0:110247f9d47e
+用户:        Christian Urban <christian dot urban at kcl dot ac dot uk>
+日期:        Thu Dec 06 15:11:21 2012 +0000
+摘要:        added
+