Quot/quotient_tacs.ML
Thu, 21 Jan 2010 19:52:46 +0100 Cezary Kaliszyk Changed fun_map and rel_map to definitions.
Thu, 21 Jan 2010 12:03:47 +0100 Cezary Kaliszyk Automatic injection of Bexeq
Thu, 21 Jan 2010 11:11:22 +0100 Cezary Kaliszyk Automatic cleaning of Bexeq<->Ex1 theorems.
Thu, 21 Jan 2010 09:55:05 +0100 Cezary Kaliszyk Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.
Thu, 21 Jan 2010 07:38:34 +0100 Cezary Kaliszyk Ex1 -> Bex1 Regularization, Preparing Exeq.
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
less more (0) -30 -10 -6 tip