Thu, 21 Jan 2010 19:52:46 +0100 | Cezary Kaliszyk | Changed fun_map and rel_map to definitions. | file | diff | annotate |
Thu, 21 Jan 2010 12:03:47 +0100 | Cezary Kaliszyk | Automatic injection of Bexeq | file | diff | annotate |
Thu, 21 Jan 2010 11:11:22 +0100 | Cezary Kaliszyk | Automatic cleaning of Bexeq<->Ex1 theorems. | file | diff | annotate |
Thu, 21 Jan 2010 09:55:05 +0100 | Cezary Kaliszyk | Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles. | file | diff | annotate |
Thu, 21 Jan 2010 07:38:34 +0100 | Cezary Kaliszyk | Ex1 -> Bex1 Regularization, Preparing Exeq. | file | diff | annotate |
Sat, 16 Jan 2010 02:09:38 +0100 | 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 |