| 2010-05-17 |
Cezary Kaliszyk |
alpha_alphabn for bindings in a type under bn.
|
file |
diff |
annotate
|
| 2010-05-12 |
Cezary Kaliszyk |
include set_simps and append_simps in fv_rsp
|
file |
diff |
annotate
|
| 2010-05-12 |
Cezary Kaliszyk |
Move alpha_eqvt to unused.
|
file |
diff |
annotate
|
| 2010-05-12 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| 2010-05-12 |
Cezary Kaliszyk |
fvbv_rsp include prod_rel.simps
|
file |
diff |
annotate
|
| 2010-05-12 |
Cezary Kaliszyk |
Use raw_induct instead of induct
|
file |
diff |
annotate
|
| 2010-05-06 |
Cezary Kaliszyk |
alpha_eqvt_tac with prod_rel and prod_fv simps
|
file |
diff |
annotate
|
| 2010-05-06 |
Cezary Kaliszyk |
prod_rel and prod_fv simps
|
file |
diff |
annotate
|
| 2010-05-03 |
Cezary Kaliszyk |
alpha_eqvt_tac fixed to work when the existential is not at the top level.
|
file |
diff |
annotate
|
| 2010-04-19 |
Christian Urban |
deleting function perm_arg in favour of the library function mk_perm
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
Accept non-equality eqvt rules in support proofs.
|
file |
diff |
annotate
|
| 2010-04-01 |
Cezary Kaliszyk |
Let with multiple bindings.
|
file |
diff |
annotate
|
| 2010-03-27 |
Cezary Kaliszyk |
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
|
file |
diff |
annotate
|
| 2010-03-27 |
Cezary Kaliszyk |
Get lifted types information from the quotient package.
|
file |
diff |
annotate
|
| 2010-03-27 |
Cezary Kaliszyk |
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
|
file |
diff |
annotate
|
| 2010-03-27 |
Cezary Kaliszyk |
Initial proof modifications for alpha_res
|
file |
diff |
annotate
|
| 2010-03-26 |
Cezary Kaliszyk |
Removed remaining cheats + some cleaning.
|
file |
diff |
annotate
|
| 2010-03-26 |
Cezary Kaliszyk |
Removed another cheat and cleaned the code a bit.
|
file |
diff |
annotate
|
| 2010-03-25 |
Cezary Kaliszyk |
Gathering things to prove by induction together; removed cheat_bn_eqvt.
|
file |
diff |
annotate
|
| 2010-03-24 |
Cezary Kaliszyk |
Export all the cheats needed for Core Haskell.
|
file |
diff |
annotate
|
| 2010-03-22 |
Cezary Kaliszyk |
Got rid of alpha_bn_rsp_cheat.
|
file |
diff |
annotate
|
| 2010-03-22 |
Cezary Kaliszyk |
alpha_bn_rsp_pre automatized.
|
file |
diff |
annotate
|
| 2010-03-22 |
Cezary Kaliszyk |
fv_rsp proved automatically.
|
file |
diff |
annotate
|
| 2010-03-20 |
Cezary Kaliszyk |
Use 'alpha_bn_refl' to get rid of one of the sorrys.
|
file |
diff |
annotate
|
| 2010-03-19 |
Cezary Kaliszyk |
Automatically derive support for datatypes with at-most one binding per constructor.
|
file |
diff |
annotate
|
| 2010-03-18 |
Cezary Kaliszyk |
Clean 'Lift', start working only on exported things in Parser.
|
file |
diff |
annotate
|
| 2010-03-17 |
Cezary Kaliszyk |
Finished all proofs in Term5 and Term5n.
|
file |
diff |
annotate
|
| 2010-03-15 |
Cezary Kaliszyk |
cheat_alpha_eqvt no longer needed; the proofs work.
|
file |
diff |
annotate
|
| 2010-03-11 |
Cezary Kaliszyk |
Lifting constants.
|
file |
diff |
annotate
|
| 2010-03-11 |
Cezary Kaliszyk |
extract build_eqvts_tac.
|
file |
diff |
annotate
|