| Mon, 03 May 2010 15:37:21 +0200 |
Cezary Kaliszyk |
alpha_eqvt_tac fixed to work when the existential is not at the top level.
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 17:26:07 +0200 |
Christian Urban |
deleting function perm_arg in favour of the library function mk_perm
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 10:35:08 +0200 |
Cezary Kaliszyk |
Accept non-equality eqvt rules in support proofs.
|
file |
diff |
annotate
|
| Thu, 01 Apr 2010 08:48:33 +0200 |
Cezary Kaliszyk |
Let with multiple bindings.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 14:55:07 +0100 |
Cezary Kaliszyk |
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 13:50:59 +0100 |
Cezary Kaliszyk |
Get lifted types information from the quotient package.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 08:42:07 +0100 |
Cezary Kaliszyk |
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 08:17:43 +0100 |
Cezary Kaliszyk |
Initial proof modifications for alpha_res
|
file |
diff |
annotate
|
| Fri, 26 Mar 2010 16:20:39 +0100 |
Cezary Kaliszyk |
Removed remaining cheats + some cleaning.
|
file |
diff |
annotate
|
| Fri, 26 Mar 2010 10:07:26 +0100 |
Cezary Kaliszyk |
Removed another cheat and cleaned the code a bit.
|
file |
diff |
annotate
|
| Thu, 25 Mar 2010 17:30:46 +0100 |
Cezary Kaliszyk |
Gathering things to prove by induction together; removed cheat_bn_eqvt.
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 10:49:50 +0100 |
Cezary Kaliszyk |
Export all the cheats needed for Core Haskell.
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 17:21:27 +0100 |
Cezary Kaliszyk |
Got rid of alpha_bn_rsp_cheat.
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 15:27:01 +0100 |
Cezary Kaliszyk |
alpha_bn_rsp_pre automatized.
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 14:07:07 +0100 |
Cezary Kaliszyk |
fv_rsp proved automatically.
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 09:27:28 +0100 |
Cezary Kaliszyk |
Use 'alpha_bn_refl' to get rid of one of the sorrys.
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 18:42:57 +0100 |
Cezary Kaliszyk |
Automatically derive support for datatypes with at-most one binding per constructor.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 07:26:36 +0100 |
Cezary Kaliszyk |
Clean 'Lift', start working only on exported things in Parser.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 11:11:25 +0100 |
Cezary Kaliszyk |
Finished all proofs in Term5 and Term5n.
|
file |
diff |
annotate
|
| Mon, 15 Mar 2010 11:50:12 +0100 |
Cezary Kaliszyk |
cheat_alpha_eqvt no longer needed; the proofs work.
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 12:26:24 +0100 |
Cezary Kaliszyk |
Lifting constants.
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 11:15:14 +0100 |
Cezary Kaliszyk |
extract build_eqvts_tac.
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 10:39:29 +0100 |
Cezary Kaliszyk |
build_eqvts no longer requires permutations.
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 10:10:23 +0100 |
Cezary Kaliszyk |
Export tactic out of alpha_eqvt.
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 17:47:29 +0100 |
Cezary Kaliszyk |
Code for solving symp goals with multiple existentials.
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 14:22:58 +0100 |
Cezary Kaliszyk |
Fix eqvt for multiple quantifiers.
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 17:11:19 +0100 |
Cezary Kaliszyk |
Include the raw eqvt lemmas.
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 15:10:47 +0100 |
Cezary Kaliszyk |
Moving wrappers out of Lift.
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 14:24:57 +0100 |
Cezary Kaliszyk |
More fixes for new alpha, the whole lift script should now work again.
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 11:04:49 +0100 |
Cezary Kaliszyk |
Fixed eqvt code.
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 15:10:55 +0100 |
Cezary Kaliszyk |
Change in signature of prove_const_rsp for general lifting.
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 12:30:50 +0100 |
Cezary Kaliszyk |
Move the eqvt code out of Terms and fixed induction for single-rule examples.
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 07:48:33 +0100 |
Christian Urban |
moved Nominal to "toplevel"
|
file |
diff |
annotate
| base
|