Fri, 16 Dec 2016 22:54:14 +0100 refactored induction principle generation code, for reuse for nonuniform datatypes
blanchet [Fri, 16 Dec 2016 22:54:14 +0100] rev 64576
refactored induction principle generation code, for reuse for nonuniform datatypes
Fri, 16 Dec 2016 19:50:46 +0100 merged
wenzelm [Fri, 16 Dec 2016 19:50:46 +0100] rev 64575
merged
Fri, 16 Dec 2016 19:07:16 +0100 consolidate nested thms with persistent result, for improved performance;
wenzelm [Fri, 16 Dec 2016 19:07:16 +0100] rev 64574
consolidate nested thms with persistent result, for improved performance; always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;
Fri, 16 Dec 2016 14:06:31 +0100 tuned signature -- more abstract type thm_node;
wenzelm [Fri, 16 Dec 2016 14:06:31 +0100] rev 64573
tuned signature -- more abstract type thm_node;
Thu, 15 Dec 2016 22:22:45 +0100 tuned signature;
wenzelm [Thu, 15 Dec 2016 22:22:45 +0100] rev 64572
tuned signature;
Thu, 15 Dec 2016 21:16:10 +0100 tuned;
wenzelm [Thu, 15 Dec 2016 21:16:10 +0100] rev 64571
tuned;
Thu, 15 Dec 2016 15:08:18 +0100 back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
wenzelm [Thu, 15 Dec 2016 15:08:18 +0100] rev 64570
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
Wed, 14 Dec 2016 18:37:54 +0100 simplified options;
wenzelm [Wed, 14 Dec 2016 18:37:54 +0100] rev 64569
simplified options;
Wed, 14 Dec 2016 18:22:18 +0100 more careful derivation_closed / close_derivation;
wenzelm [Wed, 14 Dec 2016 18:22:18 +0100] rev 64568
more careful derivation_closed / close_derivation;
Wed, 14 Dec 2016 16:59:41 +0100 always close derivation, for significantly improved performance without parallel proofs;
wenzelm [Wed, 14 Dec 2016 16:59:41 +0100] rev 64567
always close derivation, for significantly improved performance without parallel proofs;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip