Tue, 21 Jun 2011 10:39:25 +0900 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 21 Jun 2011 10:39:25 +0900] rev 2881
merge
Tue, 21 Jun 2011 10:37:43 +0900 spelling
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 21 Jun 2011 10:37:43 +0900] rev 2880
spelling
Mon, 20 Jun 2011 20:09:51 +0900 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 20:09:51 +0900] rev 2879
merge
Mon, 20 Jun 2011 20:08:16 +0900 Abs_set_fcb
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 20:08:16 +0900] rev 2878
Abs_set_fcb
Mon, 20 Jun 2011 20:09:30 +0900 function for let-rec
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 20:09:30 +0900] rev 2877
function for let-rec
Mon, 20 Jun 2011 10:16:12 +0900 TODO/minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 10:16:12 +0900] rev 2876
TODO/minor
Mon, 20 Jun 2011 09:59:18 +0900 Move lst_fcb to Nominal2_Abs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 09:59:18 +0900] rev 2875
Move lst_fcb to Nominal2_Abs
Mon, 20 Jun 2011 09:38:57 +0900 More minor TODOs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 09:38:57 +0900] rev 2874
More minor TODOs
Mon, 20 Jun 2011 09:36:16 +0900 Update TODO
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 09:36:16 +0900] rev 2873
Update TODO
Mon, 20 Jun 2011 09:29:42 +0900 Let/minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 09:29:42 +0900] rev 2872
Let/minor
Mon, 20 Jun 2011 08:50:13 +0900 Update Quotient/TODO and remove some attic code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 08:50:13 +0900] rev 2871
Update Quotient/TODO and remove some attic code
Sun, 19 Jun 2011 13:14:37 +0900 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 19 Jun 2011 13:14:37 +0900] rev 2870
merge
Sun, 19 Jun 2011 13:10:15 +0900 little on cps2
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 19 Jun 2011 13:10:15 +0900] rev 2869
little on cps2
Thu, 16 Jun 2011 20:07:03 +0100 got rid of the boolean flag in the raw_equivariance function
Christian Urban <urbanc@in.tum.de> [Thu, 16 Jun 2011 20:07:03 +0100] rev 2868
got rid of the boolean flag in the raw_equivariance function
Thu, 16 Jun 2011 23:11:50 +0900 Fix
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 16 Jun 2011 23:11:50 +0900] rev 2867
Fix
Thu, 16 Jun 2011 22:00:52 +0900 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 16 Jun 2011 22:00:52 +0900] rev 2866
merge
Thu, 16 Jun 2011 21:23:38 +0900 CPS3 can be defined with eqvt_rhs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 16 Jun 2011 21:23:38 +0900] rev 2865
CPS3 can be defined with eqvt_rhs.
Thu, 16 Jun 2011 13:32:36 +0100 moved for the moment CPS translations into the example directory
Christian Urban <urbanc@in.tum.de> [Thu, 16 Jun 2011 13:32:36 +0100] rev 2864
moved for the moment CPS translations into the example directory
Thu, 16 Jun 2011 13:14:53 +0100 merged
Christian Urban <urbanc@in.tum.de> [Thu, 16 Jun 2011 13:14:53 +0100] rev 2863
merged
Thu, 16 Jun 2011 13:14:16 +0100 added eqvt_at and invariant for boths sides of the equations
Christian Urban <urbanc@in.tum.de> [Thu, 16 Jun 2011 13:14:16 +0100] rev 2862
added eqvt_at and invariant for boths sides of the equations
Thu, 16 Jun 2011 20:56:30 +0900 Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 16 Jun 2011 20:56:30 +0900] rev 2861
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Thu, 16 Jun 2011 12:12:25 +0100 added a test that every function must be of pt-sort
Christian Urban <urbanc@in.tum.de> [Thu, 16 Jun 2011 12:12:25 +0100] rev 2860
added a test that every function must be of pt-sort
Thu, 16 Jun 2011 11:03:01 +0100 all tests work again
Christian Urban <urbanc@in.tum.de> [Thu, 16 Jun 2011 11:03:01 +0100] rev 2859
all tests work again
Wed, 15 Jun 2011 22:36:59 +0100 added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Christian Urban <urbanc@in.tum.de> [Wed, 15 Jun 2011 22:36:59 +0100] rev 2858
added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
Wed, 15 Jun 2011 12:52:48 +0100 added an abstract
Christian Urban <urbanc@in.tum.de> [Wed, 15 Jun 2011 12:52:48 +0100] rev 2857
added an abstract
Wed, 15 Jun 2011 12:32:40 +0100 added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de> [Wed, 15 Jun 2011 12:32:40 +0100] rev 2856
added a stub for function paper; "isabelle make fnpaper"
Wed, 15 Jun 2011 11:06:48 +0900 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 11:06:48 +0900] rev 2855
merge
Wed, 15 Jun 2011 11:06:31 +0900 one TODO and one Problem?
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 11:06:31 +0900] rev 2854
one TODO and one Problem?
Wed, 15 Jun 2011 09:51:26 +0900 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:51:26 +0900] rev 2853
merge
Wed, 15 Jun 2011 09:50:53 +0900 Some TODOs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:50:53 +0900] rev 2852
Some TODOs
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 tip