Tue, 14 Jun 2011 19:11:44 +0100 tuned some proofs
Christian Urban <urbanc@in.tum.de> [Tue, 14 Jun 2011 19:11:44 +0100] rev 2849
tuned some proofs
Tue, 14 Jun 2011 14:07:07 +0100 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 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
Tue, 14 Jun 2011 11:43:06 +0100 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 14 Jun 2011 11:43:06 +0100] rev 2847
tuned
Fri, 10 Jun 2011 15:52:17 +0900 Move working examples before non-working ones
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:52:17 +0900] rev 2846
Move working examples before non-working ones
Fri, 10 Jun 2011 15:45:49 +0900 Optimized proofs and removed some garbage.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:45:49 +0900] rev 2845
Optimized proofs and removed some garbage.
Fri, 10 Jun 2011 15:31:14 +0900 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 15:31:14 +0900] rev 2844
merge
Fri, 10 Jun 2011 15:30:09 +0900 Slightly modify fcb for list1 and put in common place.
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.
Fri, 10 Jun 2011 09:00:24 +0900 Experiments with Let
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 10 Jun 2011 09:00:24 +0900] rev 2842
Experiments with Let
Thu, 09 Jun 2011 15:34:51 +0900 Eval can be defined with additional freshness
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 09 Jun 2011 15:34:51 +0900] rev 2841
Eval can be defined with additional freshness
Thu, 09 Jun 2011 15:03:58 +0900 Minor simplification
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 09 Jun 2011 15:03:58 +0900] rev 2840
Minor simplification
Thu, 09 Jun 2011 11:10:41 +0900 abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 09 Jun 2011 11:10:41 +0900] rev 2839
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Thu, 09 Jun 2011 09:44:51 +0900 More experiments with 'default'
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 09 Jun 2011 09:44:51 +0900] rev 2838
More experiments with 'default'
Wed, 08 Jun 2011 21:44:03 +0900 Finished the proof with the invariant
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 21:44:03 +0900] rev 2837
Finished the proof with the invariant
Wed, 08 Jun 2011 21:32:35 +0900 Issue with 'default'
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 21:32:35 +0900] rev 2836
Issue with 'default'
Wed, 08 Jun 2011 12:30:56 +0100 merged
Christian Urban <urbanc@in.tum.de> [Wed, 08 Jun 2011 12:30:56 +0100] rev 2835
merged
Wed, 08 Jun 2011 12:30:46 +0100 merged
Christian Urban <urbanc@in.tum.de> [Wed, 08 Jun 2011 12:30:46 +0100] rev 2834
merged
Wed, 08 Jun 2011 08:44:01 +0100 using the option "default" the function package allows one to give an explicit default value
Christian Urban <urbanc@in.tum.de> [Wed, 08 Jun 2011 08:44:01 +0100] rev 2833
using the option "default" the function package allows one to give an explicit default value
Wed, 08 Jun 2011 17:52:06 +0900 Simpler proof of TypeSchemes/substs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 17:52:06 +0900] rev 2832
Simpler proof of TypeSchemes/substs
Wed, 08 Jun 2011 17:25:54 +0900 Simplify fcb_res
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 17:25:54 +0900] rev 2831
Simplify fcb_res
Wed, 08 Jun 2011 09:56:39 +0900 FCB for res binding and simplified proof of subst for type schemes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 09:56:39 +0900] rev 2830
FCB for res binding and simplified proof of subst for type schemes
Wed, 08 Jun 2011 07:06:20 +0900 Simplify ln-trans proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 07:06:20 +0900] rev 2829
Simplify ln-trans proof
Wed, 08 Jun 2011 07:02:52 +0900 cbvs can be easily defined without an invariant
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 08 Jun 2011 07:02:52 +0900] rev 2828
cbvs can be easily defined without an invariant
Tue, 07 Jun 2011 20:58:00 +0100 defined the "count-bound-variables-occurences" function which has an accumulator like trans
Christian Urban <urbanc@in.tum.de> [Tue, 07 Jun 2011 20:58:00 +0100] rev 2827
defined the "count-bound-variables-occurences" function which has an accumulator like trans
Tue, 07 Jun 2011 17:45:38 +0100 merged
Christian Urban <urbanc@in.tum.de> [Tue, 07 Jun 2011 17:45:38 +0100] rev 2826
merged
Tue, 07 Jun 2011 23:42:12 +0900 remove garbage (proofs that assumes the invariant outside function)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 07 Jun 2011 23:42:12 +0900] rev 2825
remove garbage (proofs that assumes the invariant outside function)
Tue, 07 Jun 2011 23:38:39 +0900 Proof of trans with invariant
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 07 Jun 2011 23:38:39 +0900] rev 2824
Proof of trans with invariant
Tue, 07 Jun 2011 23:22:58 +0900 Testing invariant in Lambda_F_T
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 07 Jun 2011 23:22:58 +0900] rev 2823
Testing invariant in Lambda_F_T
Tue, 07 Jun 2011 10:40:06 +0100 cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de> [Tue, 07 Jun 2011 10:40:06 +0100] rev 2822
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Tue, 07 Jun 2011 08:52:59 +0100 fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de> [Tue, 07 Jun 2011 08:52:59 +0100] rev 2821
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Mon, 06 Jun 2011 13:11:04 +0100 slightly stronger property in fundef_ex_prop
Christian Urban <urbanc@in.tum.de> [Mon, 06 Jun 2011 13:11:04 +0100] rev 2820
slightly stronger property in fundef_ex_prop
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 tip