| Wed, 20 Feb 2013 08:44:24 +0100 | blanchet | alias for people like me | changeset | files |
| Tue, 19 Feb 2013 19:44:10 +0100 | haftmann | dropped spurious left-over from 0a2371e7ced3 | changeset | files |
| Tue, 19 Feb 2013 17:01:06 +0100 | blanchet | avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs | changeset | files |
| Tue, 19 Feb 2013 15:37:42 +0100 | blanchet | interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices | changeset | files |