Sat, 28 Nov 2009 03:17:22 +0100 | Cezary Kaliszyk | Merged comment | changeset | files |
Sat, 28 Nov 2009 03:07:38 +0100 | Cezary Kaliszyk | Integrated Stefan's tactic and changed substs to simps with empty context. | changeset | files |
Sat, 28 Nov 2009 03:06:22 +0100 | Christian Urban | some slight tuning of the apply-tactic | changeset | files |
Sat, 28 Nov 2009 02:54:24 +0100 | Christian Urban | annotated a proof with all steps and simplified LAMBDA_RES_TAC | changeset | files |
Fri, 27 Nov 2009 18:38:44 +0100 | Cezary Kaliszyk | Merge | changeset | files |
Fri, 27 Nov 2009 18:38:09 +0100 | Cezary Kaliszyk | The magical code from Stefan, will need to be integrated in the Simproc. | changeset | files |
Fri, 27 Nov 2009 13:59:52 +0100 | Christian Urban | replaced FIRST' (map rtac list) with resolve_tac list | changeset | files |
Fri, 27 Nov 2009 10:04:49 +0100 | Cezary Kaliszyk | Simplifying arguments; got rid of trans2_thm. | changeset | files |