| Sun, 01 May 2011 18:37:24 +0200 | blanchet | fixed parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y)) | changeset | files |
| Sun, 01 May 2011 18:37:24 +0200 | blanchet | handle special constants correctly in Isar proof reconstruction code, especially type predicates | changeset | files |
| Sun, 01 May 2011 18:37:24 +0200 | blanchet | make sure the minimizer monomorphizes when it should | changeset | files |