| Wed, 26 Sep 2012 10:41:36 +0200 | blanchet | disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated) | changeset | files |
| Wed, 26 Sep 2012 10:01:00 +0200 | blanchet | got rid of other instance of shaky "Thm.generalize" | changeset | files |
| Wed, 26 Sep 2012 10:01:00 +0200 | blanchet | tweaked theorem names (in particular, dropped s's) | changeset | files |
| Wed, 26 Sep 2012 10:01:00 +0200 | blanchet | get rid of shaky "Thm.generalize" | changeset | files |
| Wed, 26 Sep 2012 10:01:00 +0200 | blanchet | fixed "rels" + split them into injectivity and distinctness | changeset | files |
| Wed, 26 Sep 2012 10:00:59 +0200 | blanchet | generate high-level "coinduct" and "strong_coinduct" properties | changeset | files |
| Wed, 26 Sep 2012 10:00:59 +0200 | blanchet | added coinduction tactic | changeset | files |