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
|
2010-03-11 |
Cezary Kaliszyk |
build_eqvts no longer requires permutations.
|
file |
diff |
annotate
|
2010-03-11 |
Cezary Kaliszyk |
Export tactic out of alpha_eqvt.
|
file |
diff |
annotate
|
2010-03-03 |
Cezary Kaliszyk |
Code for solving symp goals with multiple existentials.
|
file |
diff |
annotate
|
2010-03-03 |
Cezary Kaliszyk |
Fix eqvt for multiple quantifiers.
|
file |
diff |
annotate
|
2010-03-02 |
Cezary Kaliszyk |
Include the raw eqvt lemmas.
|
file |
diff |
annotate
|
2010-03-02 |
Cezary Kaliszyk |
Moving wrappers out of Lift.
|
file |
diff |
annotate
|
2010-03-02 |
Cezary Kaliszyk |
More fixes for new alpha, the whole lift script should now work again.
|
file |
diff |
annotate
|
2010-03-02 |
Cezary Kaliszyk |
Fixed eqvt code.
|
file |
diff |
annotate
|
2010-02-26 |
Cezary Kaliszyk |
Change in signature of prove_const_rsp for general lifting.
|
file |
diff |
annotate
|
2010-02-25 |
Cezary Kaliszyk |
Move the eqvt code out of Terms and fixed induction for single-rule examples.
|
file |
diff |
annotate
|
2010-02-25 |
Christian Urban |
moved Nominal to "toplevel"
|
file |
diff |
annotate
| base
|