wenzelm [Fri, 16 Dec 2016 19:50:46 +0100] rev 64575
merged
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;
wenzelm [Fri, 16 Dec 2016 14:06:31 +0100] rev 64573
tuned signature -- more abstract type thm_node;
wenzelm [Thu, 15 Dec 2016 22:22:45 +0100] rev 64572
tuned signature;
wenzelm [Thu, 15 Dec 2016 21:16:10 +0100] rev 64571
tuned;
wenzelm [Thu, 15 Dec 2016 15:08:18 +0100] rev 64570
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
wenzelm [Wed, 14 Dec 2016 18:37:54 +0100] rev 64569
simplified options;
wenzelm [Wed, 14 Dec 2016 18:22:18 +0100] rev 64568
more careful derivation_closed / close_derivation;
wenzelm [Wed, 14 Dec 2016 16:59:41 +0100] rev 64567
always close derivation, for significantly improved performance without parallel proofs;
wenzelm [Wed, 14 Dec 2016 15:48:18 +0100] rev 64566
tuned whitespace;
wenzelm [Wed, 14 Dec 2016 11:53:45 +0100] rev 64565
removed of_string_limited;
wenzelm [Wed, 14 Dec 2016 11:26:23 +0100] rev 64564
tuned;
wenzelm [Wed, 14 Dec 2016 10:40:25 +0100] rev 64563
tuned;
wenzelm [Wed, 14 Dec 2016 10:29:47 +0100] rev 64562
tuned;
blanchet [Thu, 15 Dec 2016 15:05:35 +0100] rev 64561
updated CASC instructions + tuning