Nominal/Rsp.thy
Sat, 20 Mar 2010 09:27:28 +0100 Cezary Kaliszyk Use 'alpha_bn_refl' to get rid of one of the sorrys.
Fri, 19 Mar 2010 18:42:57 +0100 Cezary Kaliszyk Automatically derive support for datatypes with at-most one binding per constructor.
Thu, 18 Mar 2010 07:26:36 +0100 Cezary Kaliszyk Clean 'Lift', start working only on exported things in Parser.
Wed, 17 Mar 2010 11:11:25 +0100 Cezary Kaliszyk Finished all proofs in Term5 and Term5n.
Mon, 15 Mar 2010 11:50:12 +0100 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work.
Thu, 11 Mar 2010 12:26:24 +0100 Cezary Kaliszyk Lifting constants.
Thu, 11 Mar 2010 11:15:14 +0100 Cezary Kaliszyk extract build_eqvts_tac.
Thu, 11 Mar 2010 10:39:29 +0100 Cezary Kaliszyk build_eqvts no longer requires permutations.
Thu, 11 Mar 2010 10:10:23 +0100 Cezary Kaliszyk Export tactic out of alpha_eqvt.
Wed, 03 Mar 2010 17:47:29 +0100 Cezary Kaliszyk Code for solving symp goals with multiple existentials.
Wed, 03 Mar 2010 14:22:58 +0100 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
Tue, 02 Mar 2010 17:11:19 +0100 Cezary Kaliszyk Include the raw eqvt lemmas.
Tue, 02 Mar 2010 15:10:47 +0100 Cezary Kaliszyk Moving wrappers out of Lift.
Tue, 02 Mar 2010 14:24:57 +0100 Cezary Kaliszyk More fixes for new alpha, the whole lift script should now work again.
less more (0) -14 tip