| 2009-12-09 |
Christian Urban |
fixed minor stupidity
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Exception handling.
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Code cleaning.
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
foldr_rsp.
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
deleted make_inst3
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
moved function and tuned comment
|
changeset |
files
|
| 2009-12-09 |
Christian Urban |
improved fun_map_conv
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Arbitrary number of fun_map_tacs.
|
changeset |
files
|
| 2009-12-09 |
Cezary Kaliszyk |
Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
tuned code
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
tuned the examples and flagged the problematic cleaning lemmas in FSet
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
manually cleaned the hard lemma.
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
decoupled QuotProd from QuotMain and also started new cleaning strategy
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
An example which is hard to lift because of the interplay between lambda_prs and unfolding.
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
proper formulation of all preservation theorems
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
started to reformulate preserve lemmas
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
properly set up the prs_rules
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
added preserve rules to the cleaning_tac
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
cleaning.
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
chnaged syntax to "lifting theorem"
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
changed names of attributes
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Manual regularization of a goal in FSet.
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
merged
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
added methods for the lifting_tac and the other tacs
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
make_inst3
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Merge
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
trans2 replaced with equals_rsp_tac
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
corrected name of FSet in ROOT.ML
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Made fset work again to test all.
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Finished the proof of ttt2 and found bug in regularize when trying ttt3.
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Another lambda example theorem proved. Seems it starts working properly.
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Proper checked map_rsp.
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Nitpick found a counterexample for one lemma.
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
It also regularizes.
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
inj_repabs also works.
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| 2009-12-08 |
Cezary Kaliszyk |
An example of working cleaning for lambda lifting. Still not sure why Babs helps.
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
tuned
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
the lift_tac produces a warning message if one of the three automatic proofs fails
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
added a thm list for ids
|
changeset |
files
|
| 2009-12-08 |
Christian Urban |
removed a fixme: map_info is now checked
|
changeset |
files
|
| 2009-12-07 |
Christian Urban |
tuning of the code
|
changeset |
files
|
| 2009-12-07 |
Christian Urban |
merged
|
changeset |
files
|