2009-12-09 |
Christian Urban |
deleted make_inst3
|
file |
diff |
annotate
|
2009-12-09 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-12-09 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-12-09 |
Christian Urban |
moved function and tuned comment
|
file |
diff |
annotate
|
2009-12-09 |
Christian Urban |
improved fun_map_conv
|
file |
diff |
annotate
|
2009-12-09 |
Cezary Kaliszyk |
Arbitrary number of fun_map_tacs.
|
file |
diff |
annotate
|
2009-12-09 |
Cezary Kaliszyk |
Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
tuned code
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
decoupled QuotProd from QuotMain and also started new cleaning strategy
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
properly set up the prs_rules
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
added preserve rules to the cleaning_tac
|
file |
diff |
annotate
|
2009-12-08 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
2009-12-08 |
Cezary Kaliszyk |
cleaning.
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
chnaged syntax to "lifting theorem"
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
changed names of attributes
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
added methods for the lifting_tac and the other tacs
|
file |
diff |
annotate
|
2009-12-08 |
Cezary Kaliszyk |
make_inst3
|
file |
diff |
annotate
|
2009-12-08 |
Cezary Kaliszyk |
trans2 replaced with equals_rsp_tac
|
file |
diff |
annotate
|
2009-12-08 |
Cezary Kaliszyk |
Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
|
file |
diff |
annotate
|
2009-12-08 |
Cezary Kaliszyk |
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
the lift_tac produces a warning message if one of the three automatic proofs fails
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
added a thm list for ids
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
removed a fixme: map_info is now checked
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
tuning of the code
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
|
file |
diff |
annotate
|
2009-12-07 |
Cezary Kaliszyk |
Handling of errors in lambda_prs_conv.
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
clarified the function examples
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
first attempt to deal with Babs in regularise and cleaning (not yet working)
|
file |
diff |
annotate
|
2009-12-07 |
Cezary Kaliszyk |
make_inst for lambda_prs where the second quotient is not identity.
|
file |
diff |
annotate
|
2009-12-07 |
Cezary Kaliszyk |
List moved after QuotMain
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
directory re-arrangement
|
file |
diff |
annotate
|