| 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 |
| Tue, 19 Feb 2013 15:03:36 +0100 | kuncar | delete also predicates on relations when hiding an implementation of an abstract type | changeset | files |
| Tue, 19 Feb 2013 13:37:07 +0100 | blanchet | reintroduced crucial sorting accidentally lost in 962190eab40d | changeset | files |
| Tue, 19 Feb 2013 13:27:33 +0100 | blanchet | compile | changeset | files |