| 2010-01-25 | Christian Urban | renamed QuotScript to QuotBase | file | diff | annotate |
| 2010-01-25 | Christian Urban | cleaned some theorems | file | diff | annotate |
| 2010-01-21 | Cezary Kaliszyk | Automatic injection of Bexeq | file | diff | annotate |
| 2010-01-21 | Cezary Kaliszyk | Using Bexeq_rsp, and manually lifted lemma with Ex1. | file | diff | annotate |
| 2010-01-21 | Cezary Kaliszyk | The missing rule. | file | diff | annotate |
| 2010-01-16 | Christian Urban | liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals | file | diff | annotate |
| 2010-01-14 | Cezary Kaliszyk | Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'. | file | diff | annotate |
| 2010-01-14 | Cezary Kaliszyk | Finished organising an efficient datastructure for qconst_info. | file | diff | annotate |