Fri, 25 Jun 2010 15:08:03 +0200 | blanchet | further reduce dependencies on "sledgehammer_fact_filter.ML" | changeset | files |
Fri, 25 Jun 2010 15:01:35 +0200 | blanchet | move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML"; | changeset | files |
Mon, 28 Jun 2010 10:39:39 +0200 | wenzelm | merged | changeset | files |
Mon, 28 Jun 2010 09:48:36 +0200 | Cezary Kaliszyk | Quotient package reverse lifting | changeset | files |
Mon, 28 Jun 2010 07:38:39 +0200 | Cezary Kaliszyk | Add reverse lifting flag to automated theorem derivation | changeset | files |
Mon, 28 Jun 2010 07:32:51 +0200 | Cezary Kaliszyk | Restrict quotient definitions to constants | changeset | files |
Sun, 27 Jun 2010 08:33:01 +0100 | Christian Urban | mixfix can be given for automatically lifted constants | changeset | files |