wenzelm [Sat, 17 Dec 2016 12:24:13 +0100] rev 64577
tuned whitespace;
tuned comments;
blanchet [Fri, 16 Dec 2016 22:54:14 +0100] rev 64576
refactored induction principle generation code, for reuse for nonuniform datatypes
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;