Mon, 02 May 2011 14:10:09 +0200 | blanchet | fixed random number invocation | changeset | files |
Mon, 02 May 2011 13:52:15 +0200 | blanchet | make sure E type information constants are given a weight, even if they don't appear anywhere else | changeset | files |
Mon, 02 May 2011 13:29:47 +0200 | blanchet | fix ROOT.ML and handle "readable_names" reference slightly more cleanly | changeset | files |
Mon, 02 May 2011 12:09:33 +0200 | blanchet | show sorts not just types in Isar proofs + tuning | changeset | files |
Mon, 02 May 2011 12:09:33 +0200 | blanchet | Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses -- parse these correctly | changeset | files |
Mon, 02 May 2011 12:09:33 +0200 | blanchet | tuning | changeset | files |