blanchet [Wed, 26 Sep 2012 10:41:36 +0200] rev 49596
disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)
blanchet [Wed, 26 Sep 2012 10:01:00 +0200] rev 49595
got rid of other instance of shaky "Thm.generalize"
blanchet [Wed, 26 Sep 2012 10:01:00 +0200] rev 49594
tweaked theorem names (in particular, dropped s's)
blanchet [Wed, 26 Sep 2012 10:01:00 +0200] rev 49593
get rid of shaky "Thm.generalize"
blanchet [Wed, 26 Sep 2012 10:01:00 +0200] rev 49592
fixed "rels" + split them into injectivity and distinctness
blanchet [Wed, 26 Sep 2012 10:00:59 +0200] rev 49591
generate high-level "coinduct" and "strong_coinduct" properties
blanchet [Wed, 26 Sep 2012 10:00:59 +0200] rev 49590
added coinduction tactic
blanchet [Wed, 26 Sep 2012 10:00:59 +0200] rev 49589
generalized tactic a bit
blanchet [Wed, 26 Sep 2012 10:00:59 +0200] rev 49588
export "dtor_map_coinduct" theorems, since they're used in one example
blanchet [Wed, 26 Sep 2012 10:00:59 +0200] rev 49587
name tuning