Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 09:29:42 +0900] rev 2872
Let/minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 20 Jun 2011 08:50:13 +0900] rev 2871
Update Quotient/TODO and remove some attic code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 19 Jun 2011 13:14:37 +0900] rev 2870
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 19 Jun 2011 13:10:15 +0900] rev 2869
little on cps2
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
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 16 Jun 2011 23:11:50 +0900] rev 2867
Fix
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 16 Jun 2011 22:00:52 +0900] rev 2866
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 16 Jun 2011 21:23:38 +0900] rev 2865
CPS3 can be defined with eqvt_rhs.
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
Christian Urban <urbanc@in.tum.de> [Thu, 16 Jun 2011 13:14:53 +0100] rev 2863
merged
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
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.
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
Christian Urban <urbanc@in.tum.de> [Thu, 16 Jun 2011 11:03:01 +0100] rev 2859
all tests work again
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
Christian Urban <urbanc@in.tum.de> [Wed, 15 Jun 2011 12:52:48 +0100] rev 2857
added an abstract
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"
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 11:06:48 +0900] rev 2855
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 11:06:31 +0900] rev 2854
one TODO and one Problem?
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:51:26 +0900] rev 2853
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:50:53 +0900] rev 2852
Some TODOs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:31:59 +0900] rev 2851
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 15 Jun 2011 09:25:36 +0900] rev 2850
TypeSchemes work with 'default'.
Christian Urban <urbanc@in.tum.de> [Tue, 14 Jun 2011 19:11:44 +0100] rev 2849
tuned some proofs
Christian Urban <urbanc@in.tum.de> [Tue, 14 Jun 2011 14:07:07 +0100] rev 2848
fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
Christian Urban <urbanc@in.tum.de> [Tue, 14 Jun 2011 11:43:06 +0100] rev 2847
tuned
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:52:17 +0900] rev 2846
Move working examples before non-working ones
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:45:49 +0900] rev 2845
Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:31:14 +0900] rev 2844
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:30:09 +0900] rev 2843
Slightly modify fcb for list1 and put in common place.